check_args /* Autogenerated */ /* curve description: 25519 */ /* requested operations: carry_mul, carry_square, carry_scmul121666, carry, add, sub, opp, selectznz, to_bytes, from_bytes */ /* n = 10 (from "10") */ /* s = 0x8000000000000000000000000000000000000000000000000000000000000000 (from "2^255") */ /* c = [(1, 19)] (from "1,19") */ /* machine_wordsize = 32 (from "32") */ #include typedef unsigned char fiat_25519_uint1; typedef signed char fiat_25519_int1; In fiat_25519_carry_square: Computed bounds (Some [Some [0x0 ~> 0x3ffffff], Some [0x0 ~> 0x1ffffff], Some [0x0 ~> 0xcee8f59cf0a40c7a3d673c28f96ba3d673c29031e8f59d30a3e5a], Some [0x0 ~> 0x1ffffff], Some [0x0 ~> 0x3ffffff], Some [0x0 ~> 0x1ffffff], Some [0x0 ~> 0x3ffffff], Some [0x0 ~> 0x1ffffff], Some [0x0 ~> 0x3ffffff], Some [0x0 ~> 0x1ffffff]]) are not tight enough (expected bounds not looser than (Some [Some [0x0 ~> 0x4666666], Some [0x0 ~> 0x2333333], Some [0x0 ~> 0x4666666], Some [0x0 ~> 0x2333333], Some [0x0 ~> 0x4666666], Some [0x0 ~> 0x2333333], Some [0x0 ~> 0x4666666], Some [0x0 ~> 0x2333333], Some [0x0 ~> 0x4666666], Some [0x0 ~> 0x2333333]])). The bounds [0x0 ~> 0xcee8f59cf0a40c7a3d673c28f96ba3d673c29031e8f59d30a3e5a] are looser than the expected bounds [0x0 ~> 0x4666666] When doing bounds analysis on the syntax tree: /* * Input Bounds: * arg1: [[0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999], [0x0 ~> 0xd333332], [0x0 ~> 0x6999999]] * Output Bounds: * out1: None */ void f(uint256 out1[10], const uint32_t arg1[10]) { uint32_t x1 = ((arg1[9]) * (uint32_t)UINT8_C(0x13)); uint32_t x2 = (x1 * (uint32_t)0x2); uint32_t x3 = ((arg1[9]) * (uint32_t)0x2); uint32_t x4 = ((arg1[8]) * (uint32_t)UINT8_C(0x13)); uint64_t x5 = (x4 * (uint64_t)0x2); uint32_t x6 = ((arg1[8]) * (uint32_t)0x2); uint32_t x7 = ((arg1[7]) * (uint32_t)UINT8_C(0x13)); uint32_t x8 = (x7 * (uint32_t)0x2); uint32_t x9 = ((arg1[7]) * (uint32_t)0x2); uint32_t x10 = ((arg1[6]) * (uint32_t)UINT8_C(0x13)); uint64_t x11 = (x10 * (uint64_t)0x2); uint32_t x12 = ((arg1[6]) * (uint32_t)0x2); uint32_t x13 = ((arg1[5]) * (uint32_t)0x2); uint32_t x14 = ((arg1[4]) * (uint32_t)0x2); uint32_t x15 = ((arg1[3]) * (uint32_t)0x2); uint32_t x16 = ((arg1[2]) * (uint32_t)0x2); uint32_t x17 = ((arg1[1]) * (uint32_t)0x2); uint512 x18 = ((uint512)((uint64_t)(arg1[9]) * (arg1[9])) << 230); uint64_t x19 = ((uint64_t)(arg1[8]) * x2); uint256 x20 = ((uint256)((uint64_t)(arg1[8]) * (arg1[8])) << 178); uint64_t x21 = ((arg1[7]) * (x2 * (uint64_t)0x2)); uint64_t x22 = ((arg1[7]) * x5); uint256 x23 = ((uint256)((uint64_t)(arg1[7]) * (arg1[7])) << 128); uint64_t x24 = ((uint64_t)(arg1[6]) * x2); uint64_t x25 = ((arg1[6]) * x5); uint64_t x26 = ((uint64_t)(arg1[6]) * x8); uint256 x27 = ((uint256)((uint64_t)(arg1[6]) * (arg1[6])) << 76); uint64_t x28 = ((arg1[5]) * (x2 * (uint64_t)0x2)); uint64_t x29 = ((arg1[5]) * x5); uint64_t x30 = ((arg1[5]) * (x8 * (uint64_t)0x2)); uint64_t x31 = ((arg1[5]) * x11); uint128 x32 = ((uint128)((uint64_t)(arg1[5]) * (arg1[5])) << 26); uint64_t x33 = ((uint64_t)(arg1[4]) * x2); uint64_t x34 = ((arg1[4]) * x5); uint64_t x35 = ((uint64_t)(arg1[4]) * x8); uint64_t x36 = ((arg1[4]) * x11); uint64_t x37 = ((uint64_t)(arg1[4]) * x13); uint64_t x38 = ((uint64_t)(arg1[4]) * (arg1[4])); uint64_t x39 = ((arg1[3]) * (x2 * (uint64_t)0x2)); uint64_t x40 = ((arg1[3]) * x5); uint64_t x41 = ((arg1[3]) * (x8 * (uint64_t)0x2)); uint64_t x42 = ((uint64_t)(arg1[3]) * x12); uint64_t x43 = ((uint64_t)(arg1[3]) * (x13 * (uint32_t)0x2)); uint64_t x44 = ((uint64_t)(arg1[3]) * x14); uint64_t x45 = ((uint64_t)(arg1[3]) * ((arg1[3]) * (uint32_t)0x2)); uint64_t x46 = ((uint64_t)(arg1[2]) * x2); uint64_t x47 = ((arg1[2]) * x5); uint64_t x48 = ((uint64_t)(arg1[2]) * x9); uint64_t x49 = ((uint64_t)(arg1[2]) * x12); uint64_t x50 = ((uint64_t)(arg1[2]) * x13); uint64_t x51 = ((uint64_t)(arg1[2]) * x14); uint64_t x52 = ((uint64_t)(arg1[2]) * x15); uint64_t x53 = ((uint64_t)(arg1[2]) * (arg1[2])); uint64_t x54 = ((arg1[1]) * (x2 * (uint64_t)0x2)); uint64_t x55 = ((uint64_t)(arg1[1]) * x6); uint64_t x56 = ((uint64_t)(arg1[1]) * (x9 * (uint32_t)0x2)); uint64_t x57 = ((uint64_t)(arg1[1]) * x12); uint64_t x58 = ((uint64_t)(arg1[1]) * (x13 * (uint32_t)0x2)); uint64_t x59 = ((uint64_t)(arg1[1]) * x14); uint64_t x60 = ((uint64_t)(arg1[1]) * (x15 * (uint32_t)0x2)); uint64_t x61 = ((uint64_t)(arg1[1]) * x16); uint64_t x62 = ((uint64_t)(arg1[1]) * ((arg1[1]) * (uint32_t)0x2)); uint64_t x63 = ((uint64_t)(arg1[0]) * x3); uint64_t x64 = ((uint64_t)(arg1[0]) * x6); uint64_t x65 = ((uint64_t)(arg1[0]) * x9); uint64_t x66 = ((uint64_t)(arg1[0]) * x12); uint64_t x67 = ((uint64_t)(arg1[0]) * x13); uint64_t x68 = ((uint64_t)(arg1[0]) * x14); uint64_t x69 = ((uint64_t)(arg1[0]) * x15); uint64_t x70 = ((uint64_t)(arg1[0]) * x16); uint64_t x71 = ((uint64_t)(arg1[0]) * x17); uint64_t x72 = ((uint64_t)(arg1[0]) * (arg1[0])); uint64_t x73 = (x72 + (x54 + (x47 + (x41 + x36)))); uint64_t x74 = (x73 >> 26); uint32_t x75 = (uint32_t)(x73 & UINT32_C(0x3ffffff)); uint512 x76 = (x63 + (x55 + (x48 + (x42 + (x37 + (x32 + (x27 + (x23 + (x20 + x18))))))))); uint64_t x77 = (x64 + (x56 + (x49 + (x43 + x38)))); uint64_t x78 = (x65 + (x57 + (x50 + (x44 + x19)))); uint64_t x79 = (x66 + (x58 + (x51 + (x45 + x21)))); uint64_t x80 = (x67 + (x59 + (x52 + (x24 + x22)))); uint64_t x81 = (x68 + (x60 + (x53 + (x28 + x25)))); uint64_t x82 = (x69 + (x61 + (x33 + (x29 + x26)))); uint64_t x83 = (x70 + (x62 + (x39 + (x34 + x30)))); uint64_t x84 = (x71 + (x46 + (x40 + (x35 + x31)))); uint64_t x85 = (x74 + x84); uint64_t x86 = (x85 >> 25); uint32_t x87 = (uint32_t)(x85 & UINT32_C(0x1ffffff)); uint64_t x88 = (x86 + x83); uint64_t x89 = (x88 >> 26); uint32_t x90 = (uint32_t)(x88 & UINT32_C(0x3ffffff)); uint64_t x91 = (x89 + x82); uint64_t x92 = (x91 >> 25); uint32_t x93 = (uint32_t)(x91 & UINT32_C(0x1ffffff)); uint64_t x94 = (x92 + x81); uint64_t x95 = (x94 >> 26); uint32_t x96 = (uint32_t)(x94 & UINT32_C(0x3ffffff)); uint64_t x97 = (x95 + x80); uint64_t x98 = (x97 >> 25); uint32_t x99 = (uint32_t)(x97 & UINT32_C(0x1ffffff)); uint64_t x100 = (x98 + x79); uint64_t x101 = (x100 >> 26); uint32_t x102 = (uint32_t)(x100 & UINT32_C(0x3ffffff)); uint64_t x103 = (x101 + x78); uint64_t x104 = (x103 >> 25); uint32_t x105 = (uint32_t)(x103 & UINT32_C(0x1ffffff)); uint64_t x106 = (x104 + x77); uint64_t x107 = (x106 >> 26); uint32_t x108 = (uint32_t)(x106 & UINT32_C(0x3ffffff)); uint512 x109 = (x107 + x76); uint512 x110 = (x109 >> 25); uint32_t x111 = (uint32_t)(x109 & UINT32_C(0x1ffffff)); uint512 x112 = (x110 * (uint512)UINT8_C(0x13)); uint512 x113 = (x75 + x112); uint256 x114 = (uint256)(x113 >> 26); uint32_t x115 = (uint32_t)(x113 & UINT32_C(0x3ffffff)); uint256 x116 = (x114 + x87); uint256 x117 = (x116 >> 25); uint32_t x118 = (uint32_t)(x116 & UINT32_C(0x1ffffff)); uint256 x119 = (x117 + x90); out1[0] = x115; out1[1] = x118; out1[2] = x119; out1[3] = x93; out1[4] = x96; out1[5] = x99; out1[6] = x102; out1[7] = x105; out1[8] = x108; out1[9] = x111; } with input bounds (Some [Some [0x0 ~> 0xd333332], Some [0x0 ~> 0x6999999], Some [0x0 ~> 0xd333332], Some [0x0 ~> 0x6999999], Some [0x0 ~> 0xd333332], Some [0x0 ~> 0x6999999], Some [0x0 ~> 0xd333332], Some [0x0 ~> 0x6999999], Some [0x0 ~> 0xd333332], Some [0x0 ~> 0x6999999]], tt).