diff options
Diffstat (limited to 'src/Specific')
17 files changed, 797 insertions, 797 deletions
diff --git a/src/Specific/IntegrationTestFreezeDisplay.log b/src/Specific/IntegrationTestFreezeDisplay.log index 9cf04d26f..e25c7e397 100644 --- a/src/Specific/IntegrationTestFreezeDisplay.log +++ b/src/Specific/IntegrationTestFreezeDisplay.log @@ -8,15 +8,15 @@ Interp-η uint64_t x19, uint8_t x20 = subborrow_u51(x17, x8, 0x7ffffffffffff); uint64_t x22, uint8_t x23 = subborrow_u51(x20, x7, 0x7ffffffffffff); uint64_t x24 = (uint64_t)cmovznz(x23, 0x0, 0xffffffffffffffffL); - uint64_t x25 = x24 & 0x7ffffffffffed; + uint64_t x25 = (x24 & 0x7ffffffffffed); uint64_t x27, uint8_t x28 = addcarryx_u51(0x0, x10, x25); - uint64_t x29 = x24 & 0x7ffffffffffff; + uint64_t x29 = (x24 & 0x7ffffffffffff); uint64_t x31, uint8_t x32 = addcarryx_u51(x28, x13, x29); - uint64_t x33 = x24 & 0x7ffffffffffff; + uint64_t x33 = (x24 & 0x7ffffffffffff); uint64_t x35, uint8_t x36 = addcarryx_u51(x32, x16, x33); - uint64_t x37 = x24 & 0x7ffffffffffff; + uint64_t x37 = (x24 & 0x7ffffffffffff); uint64_t x39, uint8_t x40 = addcarryx_u51(x36, x19, x37); - uint64_t x41 = x24 & 0x7ffffffffffff; + uint64_t x41 = (x24 & 0x7ffffffffffff); uint64_t x43, uint8_t _ = addcarryx_u51(x40, x22, x41); (Return x43, Return x39, Return x35, Return x31, Return x27)) x diff --git a/src/Specific/IntegrationTestKaratsubaMulDisplay.log b/src/Specific/IntegrationTestKaratsubaMulDisplay.log index 17db6102d..d085a6e3e 100644 --- a/src/Specific/IntegrationTestKaratsubaMulDisplay.log +++ b/src/Specific/IntegrationTestKaratsubaMulDisplay.log @@ -2,60 +2,60 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core, - uint128_t x32 = (uint128_t) (x11 + x16) * (x25 + x30) - (uint128_t) x11 * x25; - uint128_t x33 = (uint128_t) (x9 + x17) * (x25 + x30) + (uint128_t) (x11 + x16) * (x23 + x31) - ((uint128_t) x9 * x25 + (uint128_t) x11 * x23); - uint128_t x34 = (uint128_t) (x7 + x15) * (x25 + x30) + ((uint128_t) (x9 + x17) * (x23 + x31) + (uint128_t) (x11 + x16) * (x21 + x29)) - ((uint128_t) x7 * x25 + ((uint128_t) x9 * x23 + (uint128_t) x11 * x21)); - uint128_t x35 = (uint128_t) (x5 + x13) * (x25 + x30) + ((uint128_t) (x7 + x15) * (x23 + x31) + ((uint128_t) (x9 + x17) * (x21 + x29) + (uint128_t) (x11 + x16) * (x19 + x27))) - ((uint128_t) x5 * x25 + ((uint128_t) x7 * x23 + ((uint128_t) x9 * x21 + (uint128_t) x11 * x19))); - uint128_t x36 = (uint128_t) (x5 + x13) * (x23 + x31) + ((uint128_t) (x7 + x15) * (x21 + x29) + (uint128_t) (x9 + x17) * (x19 + x27)) - ((uint128_t) x5 * x23 + ((uint128_t) x7 * x21 + (uint128_t) x9 * x19)); - uint128_t x37 = (uint128_t) (x5 + x13) * (x21 + x29) + (uint128_t) (x7 + x15) * (x19 + x27) - ((uint128_t) x5 * x21 + (uint128_t) x7 * x19); - uint128_t x38 = (uint128_t) (x5 + x13) * (x19 + x27) - (uint128_t) x5 * x19; - uint128_t x39 = (uint128_t) x11 * x25 + (uint128_t) x16 * x30 + x36 + x32; - uint128_t x40 = (uint128_t) x9 * x25 + (uint128_t) x11 * x23 + ((uint128_t) x17 * x30 + (uint128_t) x16 * x31) + x37 + x33; - uint128_t x41 = (uint128_t) x7 * x25 + ((uint128_t) x9 * x23 + (uint128_t) x11 * x21) + ((uint128_t) x15 * x30 + ((uint128_t) x17 * x31 + (uint128_t) x16 * x29)) + x38 + x34; - uint128_t x42 = (uint128_t) x5 * x25 + ((uint128_t) x7 * x23 + ((uint128_t) x9 * x21 + (uint128_t) x11 * x19)) + ((uint128_t) x13 * x30 + ((uint128_t) x15 * x31 + ((uint128_t) x17 * x29 + (uint128_t) x16 * x27))); - uint128_t x43 = (uint128_t) x5 * x23 + ((uint128_t) x7 * x21 + (uint128_t) x9 * x19) + ((uint128_t) x13 * x31 + ((uint128_t) x15 * x29 + (uint128_t) x17 * x27)) + x32; - uint128_t x44 = (uint128_t) x5 * x21 + (uint128_t) x7 * x19 + ((uint128_t) x13 * x29 + (uint128_t) x15 * x27) + x33; - uint128_t x45 = (uint128_t) x5 * x19 + (uint128_t) x13 * x27 + x34; + uint128_t x32 = (((uint128_t)(x11 + x16) * (x25 + x30)) - ((uint128_t)x11 * x25)); + uint128_t x33 = ((((uint128_t)(x9 + x17) * (x25 + x30)) + ((uint128_t)(x11 + x16) * (x23 + x31))) - (((uint128_t)x9 * x25) + ((uint128_t)x11 * x23))); + uint128_t x34 = ((((uint128_t)(x7 + x15) * (x25 + x30)) + (((uint128_t)(x9 + x17) * (x23 + x31)) + ((uint128_t)(x11 + x16) * (x21 + x29)))) - (((uint128_t)x7 * x25) + (((uint128_t)x9 * x23) + ((uint128_t)x11 * x21)))); + uint128_t x35 = ((((uint128_t)(x5 + x13) * (x25 + x30)) + (((uint128_t)(x7 + x15) * (x23 + x31)) + (((uint128_t)(x9 + x17) * (x21 + x29)) + ((uint128_t)(x11 + x16) * (x19 + x27))))) - (((uint128_t)x5 * x25) + (((uint128_t)x7 * x23) + (((uint128_t)x9 * x21) + ((uint128_t)x11 * x19))))); + uint128_t x36 = ((((uint128_t)(x5 + x13) * (x23 + x31)) + (((uint128_t)(x7 + x15) * (x21 + x29)) + ((uint128_t)(x9 + x17) * (x19 + x27)))) - (((uint128_t)x5 * x23) + (((uint128_t)x7 * x21) + ((uint128_t)x9 * x19)))); + uint128_t x37 = ((((uint128_t)(x5 + x13) * (x21 + x29)) + ((uint128_t)(x7 + x15) * (x19 + x27))) - (((uint128_t)x5 * x21) + ((uint128_t)x7 * x19))); + uint128_t x38 = (((uint128_t)(x5 + x13) * (x19 + x27)) - ((uint128_t)x5 * x19)); + uint128_t x39 = (((((uint128_t)x11 * x25) + ((uint128_t)x16 * x30)) + x36) + x32); + uint128_t x40 = ((((((uint128_t)x9 * x25) + ((uint128_t)x11 * x23)) + (((uint128_t)x17 * x30) + ((uint128_t)x16 * x31))) + x37) + x33); + uint128_t x41 = ((((((uint128_t)x7 * x25) + (((uint128_t)x9 * x23) + ((uint128_t)x11 * x21))) + (((uint128_t)x15 * x30) + (((uint128_t)x17 * x31) + ((uint128_t)x16 * x29)))) + x38) + x34); + uint128_t x42 = ((((uint128_t)x5 * x25) + (((uint128_t)x7 * x23) + (((uint128_t)x9 * x21) + ((uint128_t)x11 * x19)))) + (((uint128_t)x13 * x30) + (((uint128_t)x15 * x31) + (((uint128_t)x17 * x29) + ((uint128_t)x16 * x27))))); + uint128_t x43 = (((((uint128_t)x5 * x23) + (((uint128_t)x7 * x21) + ((uint128_t)x9 * x19))) + (((uint128_t)x13 * x31) + (((uint128_t)x15 * x29) + ((uint128_t)x17 * x27)))) + x32); + uint128_t x44 = (((((uint128_t)x5 * x21) + ((uint128_t)x7 * x19)) + (((uint128_t)x13 * x29) + ((uint128_t)x15 * x27))) + x33); + uint128_t x45 = ((((uint128_t)x5 * x19) + ((uint128_t)x13 * x27)) + x34); uint64_t x46 = (uint64_t) (x42 >> 0x38); - uint64_t x47 = (uint64_t) x42 & 0xffffffffffffff; + uint64_t x47 = ((uint64_t)x42 & 0xffffffffffffff); uint64_t x48 = (uint64_t) (x35 >> 0x38); - uint64_t x49 = (uint64_t) x35 & 0xffffffffffffff; - uint128_t x50 = (uint128_t) 0x100000000000000 * x48 + x49; + uint64_t x49 = ((uint64_t)x35 & 0xffffffffffffff); + uint128_t x50 = (((uint128_t)0x100000000000000 * x48) + x49); uint64_t x51 = (uint64_t) (x50 >> 0x38); - uint64_t x52 = (uint64_t) x50 & 0xffffffffffffff; - uint128_t x53 = x45 + x51; + uint64_t x52 = ((uint64_t)x50 & 0xffffffffffffff); + uint128_t x53 = (x45 + x51); uint64_t x54 = (uint64_t) (x53 >> 0x38); - uint64_t x55 = (uint64_t) x53 & 0xffffffffffffff; - uint128_t x56 = x46 + x41 + x51; + uint64_t x55 = ((uint64_t)x53 & 0xffffffffffffff); + uint128_t x56 = ((x46 + x41) + x51); uint64_t x57 = (uint64_t) (x56 >> 0x38); - uint64_t x58 = (uint64_t) x56 & 0xffffffffffffff; - uint128_t x59 = x54 + x44; + uint64_t x58 = ((uint64_t)x56 & 0xffffffffffffff); + uint128_t x59 = (x54 + x44); uint64_t x60 = (uint64_t) (x59 >> 0x38); - uint64_t x61 = (uint64_t) x59 & 0xffffffffffffff; - uint128_t x62 = x57 + x40; + uint64_t x61 = ((uint64_t)x59 & 0xffffffffffffff); + uint128_t x62 = (x57 + x40); uint64_t x63 = (uint64_t) (x62 >> 0x38); - uint64_t x64 = (uint64_t) x62 & 0xffffffffffffff; - uint128_t x65 = x60 + x43; + uint64_t x64 = ((uint64_t)x62 & 0xffffffffffffff); + uint128_t x65 = (x60 + x43); uint64_t x66 = (uint64_t) (x65 >> 0x38); - uint64_t x67 = (uint64_t) x65 & 0xffffffffffffff; - uint128_t x68 = x63 + x39; + uint64_t x67 = ((uint64_t)x65 & 0xffffffffffffff); + uint128_t x68 = (x63 + x39); uint64_t x69 = (uint64_t) (x68 >> 0x38); - uint64_t x70 = (uint64_t) x68 & 0xffffffffffffff; - uint64_t x71 = x66 + x47; - uint64_t x72 = x71 >> 0x38; - uint64_t x73 = x71 & 0xffffffffffffff; - uint64_t x74 = x69 + x52; - uint64_t x75 = x74 >> 0x38; - uint64_t x76 = x74 & 0xffffffffffffff; - uint64_t x77 = 0x100000000000000 * x75 + x76; - uint64_t x78 = x77 >> 0x38; - uint64_t x79 = x77 & 0xffffffffffffff; - uint64_t x80 = x72 + x58 + x78; - uint64_t x81 = x80 >> 0x38; - uint64_t x82 = x80 & 0xffffffffffffff; - uint64_t x83 = x55 + x78; - uint64_t x84 = x83 >> 0x38; - uint64_t x85 = x83 & 0xffffffffffffff; - return (Return x79, Return x70, x81 + x64, Return x82, Return x73, Return x67, x84 + x61, Return x85)) + uint64_t x70 = ((uint64_t)x68 & 0xffffffffffffff); + uint64_t x71 = (x66 + x47); + uint64_t x72 = (x71 >> 0x38); + uint64_t x73 = (x71 & 0xffffffffffffff); + uint64_t x74 = (x69 + x52); + uint64_t x75 = (x74 >> 0x38); + uint64_t x76 = (x74 & 0xffffffffffffff); + uint64_t x77 = ((0x100000000000000 * x75) + x76); + uint64_t x78 = (x77 >> 0x38); + uint64_t x79 = (x77 & 0xffffffffffffff); + uint64_t x80 = ((x72 + x58) + x78); + uint64_t x81 = (x80 >> 0x38); + uint64_t x82 = (x80 & 0xffffffffffffff); + uint64_t x83 = (x55 + x78); + uint64_t x84 = (x83 >> 0x38); + uint64_t x85 = (x83 & 0xffffffffffffff); + return (Return x79, Return x70, (x81 + x64), Return x82, Return x73, Return x67, (x84 + x61), Return x85)) (x, x0)%core : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/IntegrationTestLadderstep130Display.log b/src/Specific/IntegrationTestLadderstep130Display.log index 95f2237c0..deff79fe1 100644 --- a/src/Specific/IntegrationTestLadderstep130Display.log +++ b/src/Specific/IntegrationTestLadderstep130Display.log @@ -2,216 +2,216 @@ let (a, b) := Interp-η (λ var : Syntax.base_type → Type, λ '(x11, x12, x10, (x17, x18, x16, (x21, x22, x20)), (x27, x28, x26, (x31, x32, x30)))%core, - uint128_t x33 = x17 + x21; - uint128_t x34 = x18 + x22; - uint128_t x35 = x16 + x20; - uint128_t x36 = 0x3ffffffffffffffffffffeL + x17 - x21; - uint128_t x37 = 0x3ffffffffffffffffffffeL + x18 - x22; - uint128_t x38 = 0x3ffffffffffffffffffff6L + x16 - x20; - uint256_t x39 = (uint256_t) x35 * x33 + ((uint256_t) x34 * x34 + (uint256_t) x33 * x35); - uint256_t x40 = (uint256_t) x35 * x34 + (uint256_t) x34 * x35 + 0x5 * ((uint256_t) x33 * x33); - uint256_t x41 = (uint256_t) x35 * x35 + 0x5 * ((uint256_t) x34 * x33 + (uint256_t) x33 * x34); + uint128_t x33 = (x17 + x21); + uint128_t x34 = (x18 + x22); + uint128_t x35 = (x16 + x20); + uint128_t x36 = ((0x3ffffffffffffffffffffeL + x17) - x21); + uint128_t x37 = ((0x3ffffffffffffffffffffeL + x18) - x22); + uint128_t x38 = ((0x3ffffffffffffffffffff6L + x16) - x20); + uint256_t x39 = (((uint256_t)x35 * x33) + (((uint256_t)x34 * x34) + ((uint256_t)x33 * x35))); + uint256_t x40 = ((((uint256_t)x35 * x34) + ((uint256_t)x34 * x35)) + (0x5 * ((uint256_t)x33 * x33))); + uint256_t x41 = (((uint256_t)x35 * x35) + (0x5 * (((uint256_t)x34 * x33) + ((uint256_t)x33 * x34)))); uint128_t x42 = (uint128_t) (x41 >> 0x55); - uint128_t x43 = (uint128_t) x41 & 0x1fffffffffffffffffffffL; - uint256_t x44 = x42 + x40; + uint128_t x43 = ((uint128_t)x41 & 0x1fffffffffffffffffffffL); + uint256_t x44 = (x42 + x40); uint128_t x45 = (uint128_t) (x44 >> 0x55); - uint128_t x46 = (uint128_t) x44 & 0x1fffffffffffffffffffffL; - uint256_t x47 = x45 + x39; + uint128_t x46 = ((uint128_t)x44 & 0x1fffffffffffffffffffffL); + uint256_t x47 = (x45 + x39); uint128_t x48 = (uint128_t) (x47 >> 0x55); - uint128_t x49 = (uint128_t) x47 & 0x1fffffffffffffffffffffL; - uint128_t x50 = x43 + 0x5 * x48; - uint128_t x51 = x50 >> 0x55; - uint128_t x52 = x50 & 0x1fffffffffffffffffffffL; - uint128_t x53 = x51 + x46; - uint128_t x54 = x53 >> 0x55; - uint128_t x55 = x53 & 0x1fffffffffffffffffffffL; - uint128_t x56 = x54 + x49; - uint256_t x57 = (uint256_t) x38 * x36 + ((uint256_t) x37 * x37 + (uint256_t) x36 * x38); - uint256_t x58 = (uint256_t) x38 * x37 + (uint256_t) x37 * x38 + 0x5 * ((uint256_t) x36 * x36); - uint256_t x59 = (uint256_t) x38 * x38 + 0x5 * ((uint256_t) x37 * x36 + (uint256_t) x36 * x37); + uint128_t x49 = ((uint128_t)x47 & 0x1fffffffffffffffffffffL); + uint128_t x50 = (x43 + (0x5 * x48)); + uint128_t x51 = (x50 >> 0x55); + uint128_t x52 = (x50 & 0x1fffffffffffffffffffffL); + uint128_t x53 = (x51 + x46); + uint128_t x54 = (x53 >> 0x55); + uint128_t x55 = (x53 & 0x1fffffffffffffffffffffL); + uint128_t x56 = (x54 + x49); + uint256_t x57 = (((uint256_t)x38 * x36) + (((uint256_t)x37 * x37) + ((uint256_t)x36 * x38))); + uint256_t x58 = ((((uint256_t)x38 * x37) + ((uint256_t)x37 * x38)) + (0x5 * ((uint256_t)x36 * x36))); + uint256_t x59 = (((uint256_t)x38 * x38) + (0x5 * (((uint256_t)x37 * x36) + ((uint256_t)x36 * x37)))); uint128_t x60 = (uint128_t) (x59 >> 0x55); - uint128_t x61 = (uint128_t) x59 & 0x1fffffffffffffffffffffL; - uint256_t x62 = x60 + x58; + uint128_t x61 = ((uint128_t)x59 & 0x1fffffffffffffffffffffL); + uint256_t x62 = (x60 + x58); uint128_t x63 = (uint128_t) (x62 >> 0x55); - uint128_t x64 = (uint128_t) x62 & 0x1fffffffffffffffffffffL; - uint256_t x65 = x63 + x57; + uint128_t x64 = ((uint128_t)x62 & 0x1fffffffffffffffffffffL); + uint256_t x65 = (x63 + x57); uint128_t x66 = (uint128_t) (x65 >> 0x55); - uint128_t x67 = (uint128_t) x65 & 0x1fffffffffffffffffffffL; - uint128_t x68 = x61 + 0x5 * x66; - uint128_t x69 = x68 >> 0x55; - uint128_t x70 = x68 & 0x1fffffffffffffffffffffL; - uint128_t x71 = x69 + x64; - uint128_t x72 = x71 >> 0x55; - uint128_t x73 = x71 & 0x1fffffffffffffffffffffL; - uint128_t x74 = x72 + x67; - uint256_t x75 = (uint256_t) x52 * x74 + ((uint256_t) x55 * x73 + (uint256_t) x56 * x70); - uint256_t x76 = (uint256_t) x52 * x73 + (uint256_t) x55 * x70 + 0x5 * ((uint256_t) x56 * x74); - uint256_t x77 = (uint256_t) x52 * x70 + 0x5 * ((uint256_t) x55 * x74 + (uint256_t) x56 * x73); + uint128_t x67 = ((uint128_t)x65 & 0x1fffffffffffffffffffffL); + uint128_t x68 = (x61 + (0x5 * x66)); + uint128_t x69 = (x68 >> 0x55); + uint128_t x70 = (x68 & 0x1fffffffffffffffffffffL); + uint128_t x71 = (x69 + x64); + uint128_t x72 = (x71 >> 0x55); + uint128_t x73 = (x71 & 0x1fffffffffffffffffffffL); + uint128_t x74 = (x72 + x67); + uint256_t x75 = (((uint256_t)x52 * x74) + (((uint256_t)x55 * x73) + ((uint256_t)x56 * x70))); + uint256_t x76 = ((((uint256_t)x52 * x73) + ((uint256_t)x55 * x70)) + (0x5 * ((uint256_t)x56 * x74))); + uint256_t x77 = (((uint256_t)x52 * x70) + (0x5 * (((uint256_t)x55 * x74) + ((uint256_t)x56 * x73)))); uint128_t x78 = (uint128_t) (x77 >> 0x55); - uint128_t x79 = (uint128_t) x77 & 0x1fffffffffffffffffffffL; - uint256_t x80 = x78 + x76; + uint128_t x79 = ((uint128_t)x77 & 0x1fffffffffffffffffffffL); + uint256_t x80 = (x78 + x76); uint128_t x81 = (uint128_t) (x80 >> 0x55); - uint128_t x82 = (uint128_t) x80 & 0x1fffffffffffffffffffffL; - uint256_t x83 = x81 + x75; + uint128_t x82 = ((uint128_t)x80 & 0x1fffffffffffffffffffffL); + uint256_t x83 = (x81 + x75); uint128_t x84 = (uint128_t) (x83 >> 0x55); - uint128_t x85 = (uint128_t) x83 & 0x1fffffffffffffffffffffL; - uint128_t x86 = x79 + 0x5 * x84; - uint128_t x87 = x86 >> 0x55; - uint128_t x88 = x86 & 0x1fffffffffffffffffffffL; - uint128_t x89 = x87 + x82; - uint128_t x90 = x89 >> 0x55; - uint128_t x91 = x89 & 0x1fffffffffffffffffffffL; - uint128_t x92 = x90 + x85; - uint128_t x93 = 0x3ffffffffffffffffffffeL + x56 - x74; - uint128_t x94 = 0x3ffffffffffffffffffffeL + x55 - x73; - uint128_t x95 = 0x3ffffffffffffffffffff6L + x52 - x70; - uint128_t x96 = 0x1db41 * x93; - uint128_t x97 = 0x1db41 * x94; - uint128_t x98 = 0x1db41 * x95; - uint128_t x99 = x98 >> 0x55; - uint128_t x100 = x98 & 0x1fffffffffffffffffffffL; - uint128_t x101 = x99 + x97; - uint128_t x102 = x101 >> 0x55; - uint128_t x103 = x101 & 0x1fffffffffffffffffffffL; - uint128_t x104 = x102 + x96; - uint128_t x105 = x104 >> 0x55; - uint128_t x106 = x104 & 0x1fffffffffffffffffffffL; - uint128_t x107 = x100 + 0x5 * x105; - uint128_t x108 = x107 >> 0x55; - uint128_t x109 = x107 & 0x1fffffffffffffffffffffL; - uint128_t x110 = x108 + x103; - uint128_t x111 = x110 >> 0x55; - uint128_t x112 = x110 & 0x1fffffffffffffffffffffL; - uint128_t x113 = x111 + x106; - uint128_t x114 = x56 + x113; - uint128_t x115 = x55 + x112; - uint128_t x116 = x52 + x109; - uint256_t x117 = (uint256_t) x95 * x114 + ((uint256_t) x94 * x115 + (uint256_t) x93 * x116); - uint256_t x118 = (uint256_t) x95 * x115 + (uint256_t) x94 * x116 + 0x5 * ((uint256_t) x93 * x114); - uint256_t x119 = (uint256_t) x95 * x116 + 0x5 * ((uint256_t) x94 * x114 + (uint256_t) x93 * x115); + uint128_t x85 = ((uint128_t)x83 & 0x1fffffffffffffffffffffL); + uint128_t x86 = (x79 + (0x5 * x84)); + uint128_t x87 = (x86 >> 0x55); + uint128_t x88 = (x86 & 0x1fffffffffffffffffffffL); + uint128_t x89 = (x87 + x82); + uint128_t x90 = (x89 >> 0x55); + uint128_t x91 = (x89 & 0x1fffffffffffffffffffffL); + uint128_t x92 = (x90 + x85); + uint128_t x93 = ((0x3ffffffffffffffffffffeL + x56) - x74); + uint128_t x94 = ((0x3ffffffffffffffffffffeL + x55) - x73); + uint128_t x95 = ((0x3ffffffffffffffffffff6L + x52) - x70); + uint128_t x96 = (0x1db41 * x93); + uint128_t x97 = (0x1db41 * x94); + uint128_t x98 = (0x1db41 * x95); + uint128_t x99 = (x98 >> 0x55); + uint128_t x100 = (x98 & 0x1fffffffffffffffffffffL); + uint128_t x101 = (x99 + x97); + uint128_t x102 = (x101 >> 0x55); + uint128_t x103 = (x101 & 0x1fffffffffffffffffffffL); + uint128_t x104 = (x102 + x96); + uint128_t x105 = (x104 >> 0x55); + uint128_t x106 = (x104 & 0x1fffffffffffffffffffffL); + uint128_t x107 = (x100 + (0x5 * x105)); + uint128_t x108 = (x107 >> 0x55); + uint128_t x109 = (x107 & 0x1fffffffffffffffffffffL); + uint128_t x110 = (x108 + x103); + uint128_t x111 = (x110 >> 0x55); + uint128_t x112 = (x110 & 0x1fffffffffffffffffffffL); + uint128_t x113 = (x111 + x106); + uint128_t x114 = (x56 + x113); + uint128_t x115 = (x55 + x112); + uint128_t x116 = (x52 + x109); + uint256_t x117 = (((uint256_t)x95 * x114) + (((uint256_t)x94 * x115) + ((uint256_t)x93 * x116))); + uint256_t x118 = ((((uint256_t)x95 * x115) + ((uint256_t)x94 * x116)) + (0x5 * ((uint256_t)x93 * x114))); + uint256_t x119 = (((uint256_t)x95 * x116) + (0x5 * (((uint256_t)x94 * x114) + ((uint256_t)x93 * x115)))); uint128_t x120 = (uint128_t) (x119 >> 0x55); - uint128_t x121 = (uint128_t) x119 & 0x1fffffffffffffffffffffL; - uint256_t x122 = x120 + x118; + uint128_t x121 = ((uint128_t)x119 & 0x1fffffffffffffffffffffL); + uint256_t x122 = (x120 + x118); uint128_t x123 = (uint128_t) (x122 >> 0x55); - uint128_t x124 = (uint128_t) x122 & 0x1fffffffffffffffffffffL; - uint256_t x125 = x123 + x117; + uint128_t x124 = ((uint128_t)x122 & 0x1fffffffffffffffffffffL); + uint256_t x125 = (x123 + x117); uint128_t x126 = (uint128_t) (x125 >> 0x55); - uint128_t x127 = (uint128_t) x125 & 0x1fffffffffffffffffffffL; - uint128_t x128 = x121 + 0x5 * x126; - uint128_t x129 = x128 >> 0x55; - uint128_t x130 = x128 & 0x1fffffffffffffffffffffL; - uint128_t x131 = x129 + x124; - uint128_t x132 = x131 >> 0x55; - uint128_t x133 = x131 & 0x1fffffffffffffffffffffL; - uint128_t x134 = x132 + x127; - uint128_t x135 = x27 + x31; - uint128_t x136 = x28 + x32; - uint128_t x137 = x26 + x30; - uint128_t x138 = 0x3ffffffffffffffffffffeL + x27 - x31; - uint128_t x139 = 0x3ffffffffffffffffffffeL + x28 - x32; - uint128_t x140 = 0x3ffffffffffffffffffff6L + x26 - x30; - uint256_t x141 = (uint256_t) x137 * x36 + ((uint256_t) x136 * x37 + (uint256_t) x135 * x38); - uint256_t x142 = (uint256_t) x137 * x37 + (uint256_t) x136 * x38 + 0x5 * ((uint256_t) x135 * x36); - uint256_t x143 = (uint256_t) x137 * x38 + 0x5 * ((uint256_t) x136 * x36 + (uint256_t) x135 * x37); + uint128_t x127 = ((uint128_t)x125 & 0x1fffffffffffffffffffffL); + uint128_t x128 = (x121 + (0x5 * x126)); + uint128_t x129 = (x128 >> 0x55); + uint128_t x130 = (x128 & 0x1fffffffffffffffffffffL); + uint128_t x131 = (x129 + x124); + uint128_t x132 = (x131 >> 0x55); + uint128_t x133 = (x131 & 0x1fffffffffffffffffffffL); + uint128_t x134 = (x132 + x127); + uint128_t x135 = (x27 + x31); + uint128_t x136 = (x28 + x32); + uint128_t x137 = (x26 + x30); + uint128_t x138 = ((0x3ffffffffffffffffffffeL + x27) - x31); + uint128_t x139 = ((0x3ffffffffffffffffffffeL + x28) - x32); + uint128_t x140 = ((0x3ffffffffffffffffffff6L + x26) - x30); + uint256_t x141 = (((uint256_t)x137 * x36) + (((uint256_t)x136 * x37) + ((uint256_t)x135 * x38))); + uint256_t x142 = ((((uint256_t)x137 * x37) + ((uint256_t)x136 * x38)) + (0x5 * ((uint256_t)x135 * x36))); + uint256_t x143 = (((uint256_t)x137 * x38) + (0x5 * (((uint256_t)x136 * x36) + ((uint256_t)x135 * x37)))); uint128_t x144 = (uint128_t) (x143 >> 0x55); - uint128_t x145 = (uint128_t) x143 & 0x1fffffffffffffffffffffL; - uint256_t x146 = x144 + x142; + uint128_t x145 = ((uint128_t)x143 & 0x1fffffffffffffffffffffL); + uint256_t x146 = (x144 + x142); uint128_t x147 = (uint128_t) (x146 >> 0x55); - uint128_t x148 = (uint128_t) x146 & 0x1fffffffffffffffffffffL; - uint256_t x149 = x147 + x141; + uint128_t x148 = ((uint128_t)x146 & 0x1fffffffffffffffffffffL); + uint256_t x149 = (x147 + x141); uint128_t x150 = (uint128_t) (x149 >> 0x55); - uint128_t x151 = (uint128_t) x149 & 0x1fffffffffffffffffffffL; - uint128_t x152 = x145 + 0x5 * x150; - uint128_t x153 = x152 >> 0x55; - uint128_t x154 = x152 & 0x1fffffffffffffffffffffL; - uint128_t x155 = x153 + x148; - uint128_t x156 = x155 >> 0x55; - uint128_t x157 = x155 & 0x1fffffffffffffffffffffL; - uint128_t x158 = x156 + x151; - uint256_t x159 = (uint256_t) x140 * x33 + ((uint256_t) x139 * x34 + (uint256_t) x138 * x35); - uint256_t x160 = (uint256_t) x140 * x34 + (uint256_t) x139 * x35 + 0x5 * ((uint256_t) x138 * x33); - uint256_t x161 = (uint256_t) x140 * x35 + 0x5 * ((uint256_t) x139 * x33 + (uint256_t) x138 * x34); + uint128_t x151 = ((uint128_t)x149 & 0x1fffffffffffffffffffffL); + uint128_t x152 = (x145 + (0x5 * x150)); + uint128_t x153 = (x152 >> 0x55); + uint128_t x154 = (x152 & 0x1fffffffffffffffffffffL); + uint128_t x155 = (x153 + x148); + uint128_t x156 = (x155 >> 0x55); + uint128_t x157 = (x155 & 0x1fffffffffffffffffffffL); + uint128_t x158 = (x156 + x151); + uint256_t x159 = (((uint256_t)x140 * x33) + (((uint256_t)x139 * x34) + ((uint256_t)x138 * x35))); + uint256_t x160 = ((((uint256_t)x140 * x34) + ((uint256_t)x139 * x35)) + (0x5 * ((uint256_t)x138 * x33))); + uint256_t x161 = (((uint256_t)x140 * x35) + (0x5 * (((uint256_t)x139 * x33) + ((uint256_t)x138 * x34)))); uint128_t x162 = (uint128_t) (x161 >> 0x55); - uint128_t x163 = (uint128_t) x161 & 0x1fffffffffffffffffffffL; - uint256_t x164 = x162 + x160; + uint128_t x163 = ((uint128_t)x161 & 0x1fffffffffffffffffffffL); + uint256_t x164 = (x162 + x160); uint128_t x165 = (uint128_t) (x164 >> 0x55); - uint128_t x166 = (uint128_t) x164 & 0x1fffffffffffffffffffffL; - uint256_t x167 = x165 + x159; + uint128_t x166 = ((uint128_t)x164 & 0x1fffffffffffffffffffffL); + uint256_t x167 = (x165 + x159); uint128_t x168 = (uint128_t) (x167 >> 0x55); - uint128_t x169 = (uint128_t) x167 & 0x1fffffffffffffffffffffL; - uint128_t x170 = x163 + 0x5 * x168; - uint128_t x171 = x170 >> 0x55; - uint128_t x172 = x170 & 0x1fffffffffffffffffffffL; - uint128_t x173 = x171 + x166; - uint128_t x174 = x173 >> 0x55; - uint128_t x175 = x173 & 0x1fffffffffffffffffffffL; - uint128_t x176 = x174 + x169; - uint128_t x177 = x176 + x158; - uint128_t x178 = x175 + x157; - uint128_t x179 = x172 + x154; - uint128_t x180 = x176 + x158; - uint128_t x181 = x175 + x157; - uint128_t x182 = x172 + x154; - uint256_t x183 = (uint256_t) x179 * x180 + ((uint256_t) x178 * x181 + (uint256_t) x177 * x182); - uint256_t x184 = (uint256_t) x179 * x181 + (uint256_t) x178 * x182 + 0x5 * ((uint256_t) x177 * x180); - uint256_t x185 = (uint256_t) x179 * x182 + 0x5 * ((uint256_t) x178 * x180 + (uint256_t) x177 * x181); + uint128_t x169 = ((uint128_t)x167 & 0x1fffffffffffffffffffffL); + uint128_t x170 = (x163 + (0x5 * x168)); + uint128_t x171 = (x170 >> 0x55); + uint128_t x172 = (x170 & 0x1fffffffffffffffffffffL); + uint128_t x173 = (x171 + x166); + uint128_t x174 = (x173 >> 0x55); + uint128_t x175 = (x173 & 0x1fffffffffffffffffffffL); + uint128_t x176 = (x174 + x169); + uint128_t x177 = (x176 + x158); + uint128_t x178 = (x175 + x157); + uint128_t x179 = (x172 + x154); + uint128_t x180 = (x176 + x158); + uint128_t x181 = (x175 + x157); + uint128_t x182 = (x172 + x154); + uint256_t x183 = (((uint256_t)x179 * x180) + (((uint256_t)x178 * x181) + ((uint256_t)x177 * x182))); + uint256_t x184 = ((((uint256_t)x179 * x181) + ((uint256_t)x178 * x182)) + (0x5 * ((uint256_t)x177 * x180))); + uint256_t x185 = (((uint256_t)x179 * x182) + (0x5 * (((uint256_t)x178 * x180) + ((uint256_t)x177 * x181)))); uint128_t x186 = (uint128_t) (x185 >> 0x55); - uint128_t x187 = (uint128_t) x185 & 0x1fffffffffffffffffffffL; - uint256_t x188 = x186 + x184; + uint128_t x187 = ((uint128_t)x185 & 0x1fffffffffffffffffffffL); + uint256_t x188 = (x186 + x184); uint128_t x189 = (uint128_t) (x188 >> 0x55); - uint128_t x190 = (uint128_t) x188 & 0x1fffffffffffffffffffffL; - uint256_t x191 = x189 + x183; + uint128_t x190 = ((uint128_t)x188 & 0x1fffffffffffffffffffffL); + uint256_t x191 = (x189 + x183); uint128_t x192 = (uint128_t) (x191 >> 0x55); - uint128_t x193 = (uint128_t) x191 & 0x1fffffffffffffffffffffL; - uint128_t x194 = x187 + 0x5 * x192; - uint128_t x195 = x194 >> 0x55; - uint128_t x196 = x194 & 0x1fffffffffffffffffffffL; - uint128_t x197 = x195 + x190; - uint128_t x198 = x197 >> 0x55; - uint128_t x199 = x197 & 0x1fffffffffffffffffffffL; - uint128_t x200 = x198 + x193; - uint128_t x201 = 0x3ffffffffffffffffffffeL + x176 - x158; - uint128_t x202 = 0x3ffffffffffffffffffffeL + x175 - x157; - uint128_t x203 = 0x3ffffffffffffffffffff6L + x172 - x154; - uint128_t x204 = 0x3ffffffffffffffffffffeL + x176 - x158; - uint128_t x205 = 0x3ffffffffffffffffffffeL + x175 - x157; - uint128_t x206 = 0x3ffffffffffffffffffff6L + x172 - x154; - uint256_t x207 = (uint256_t) x203 * x204 + ((uint256_t) x202 * x205 + (uint256_t) x201 * x206); - uint256_t x208 = (uint256_t) x203 * x205 + (uint256_t) x202 * x206 + 0x5 * ((uint256_t) x201 * x204); - uint256_t x209 = (uint256_t) x203 * x206 + 0x5 * ((uint256_t) x202 * x204 + (uint256_t) x201 * x205); + uint128_t x193 = ((uint128_t)x191 & 0x1fffffffffffffffffffffL); + uint128_t x194 = (x187 + (0x5 * x192)); + uint128_t x195 = (x194 >> 0x55); + uint128_t x196 = (x194 & 0x1fffffffffffffffffffffL); + uint128_t x197 = (x195 + x190); + uint128_t x198 = (x197 >> 0x55); + uint128_t x199 = (x197 & 0x1fffffffffffffffffffffL); + uint128_t x200 = (x198 + x193); + uint128_t x201 = ((0x3ffffffffffffffffffffeL + x176) - x158); + uint128_t x202 = ((0x3ffffffffffffffffffffeL + x175) - x157); + uint128_t x203 = ((0x3ffffffffffffffffffff6L + x172) - x154); + uint128_t x204 = ((0x3ffffffffffffffffffffeL + x176) - x158); + uint128_t x205 = ((0x3ffffffffffffffffffffeL + x175) - x157); + uint128_t x206 = ((0x3ffffffffffffffffffff6L + x172) - x154); + uint256_t x207 = (((uint256_t)x203 * x204) + (((uint256_t)x202 * x205) + ((uint256_t)x201 * x206))); + uint256_t x208 = ((((uint256_t)x203 * x205) + ((uint256_t)x202 * x206)) + (0x5 * ((uint256_t)x201 * x204))); + uint256_t x209 = (((uint256_t)x203 * x206) + (0x5 * (((uint256_t)x202 * x204) + ((uint256_t)x201 * x205)))); uint128_t x210 = (uint128_t) (x209 >> 0x55); - uint128_t x211 = (uint128_t) x209 & 0x1fffffffffffffffffffffL; - uint256_t x212 = x210 + x208; + uint128_t x211 = ((uint128_t)x209 & 0x1fffffffffffffffffffffL); + uint256_t x212 = (x210 + x208); uint128_t x213 = (uint128_t) (x212 >> 0x55); - uint128_t x214 = (uint128_t) x212 & 0x1fffffffffffffffffffffL; - uint256_t x215 = x213 + x207; + uint128_t x214 = ((uint128_t)x212 & 0x1fffffffffffffffffffffL); + uint256_t x215 = (x213 + x207); uint128_t x216 = (uint128_t) (x215 >> 0x55); - uint128_t x217 = (uint128_t) x215 & 0x1fffffffffffffffffffffL; - uint128_t x218 = x211 + 0x5 * x216; - uint128_t x219 = x218 >> 0x55; - uint128_t x220 = x218 & 0x1fffffffffffffffffffffL; - uint128_t x221 = x219 + x214; - uint128_t x222 = x221 >> 0x55; - uint128_t x223 = x221 & 0x1fffffffffffffffffffffL; - uint128_t x224 = x222 + x217; - uint256_t x225 = (uint256_t) x10 * x224 + ((uint256_t) x12 * x223 + (uint256_t) x11 * x220); - uint256_t x226 = (uint256_t) x10 * x223 + (uint256_t) x12 * x220 + 0x5 * ((uint256_t) x11 * x224); - uint256_t x227 = (uint256_t) x10 * x220 + 0x5 * ((uint256_t) x12 * x224 + (uint256_t) x11 * x223); + uint128_t x217 = ((uint128_t)x215 & 0x1fffffffffffffffffffffL); + uint128_t x218 = (x211 + (0x5 * x216)); + uint128_t x219 = (x218 >> 0x55); + uint128_t x220 = (x218 & 0x1fffffffffffffffffffffL); + uint128_t x221 = (x219 + x214); + uint128_t x222 = (x221 >> 0x55); + uint128_t x223 = (x221 & 0x1fffffffffffffffffffffL); + uint128_t x224 = (x222 + x217); + uint256_t x225 = (((uint256_t)x10 * x224) + (((uint256_t)x12 * x223) + ((uint256_t)x11 * x220))); + uint256_t x226 = ((((uint256_t)x10 * x223) + ((uint256_t)x12 * x220)) + (0x5 * ((uint256_t)x11 * x224))); + uint256_t x227 = (((uint256_t)x10 * x220) + (0x5 * (((uint256_t)x12 * x224) + ((uint256_t)x11 * x223)))); uint128_t x228 = (uint128_t) (x227 >> 0x55); - uint128_t x229 = (uint128_t) x227 & 0x1fffffffffffffffffffffL; - uint256_t x230 = x228 + x226; + uint128_t x229 = ((uint128_t)x227 & 0x1fffffffffffffffffffffL); + uint256_t x230 = (x228 + x226); uint128_t x231 = (uint128_t) (x230 >> 0x55); - uint128_t x232 = (uint128_t) x230 & 0x1fffffffffffffffffffffL; - uint256_t x233 = x231 + x225; + uint128_t x232 = ((uint128_t)x230 & 0x1fffffffffffffffffffffL); + uint256_t x233 = (x231 + x225); uint128_t x234 = (uint128_t) (x233 >> 0x55); - uint128_t x235 = (uint128_t) x233 & 0x1fffffffffffffffffffffL; - uint128_t x236 = x229 + 0x5 * x234; - uint128_t x237 = x236 >> 0x55; - uint128_t x238 = x236 & 0x1fffffffffffffffffffffL; - uint128_t x239 = x237 + x232; - uint128_t x240 = x239 >> 0x55; - uint128_t x241 = x239 & 0x1fffffffffffffffffffffL; - uint128_t x242 = x240 + x235; + uint128_t x235 = ((uint128_t)x233 & 0x1fffffffffffffffffffffL); + uint128_t x236 = (x229 + (0x5 * x234)); + uint128_t x237 = (x236 >> 0x55); + uint128_t x238 = (x236 & 0x1fffffffffffffffffffffL); + uint128_t x239 = (x237 + x232); + uint128_t x240 = (x239 >> 0x55); + uint128_t x241 = (x239 & 0x1fffffffffffffffffffffL); + uint128_t x242 = (x240 + x235); return (Return x92, Return x91, Return x88, (Return x134, Return x133, Return x130), (Return x200, Return x199, Return x196, (Return x242, Return x241, Return x238)))) (x, (x0, x1), (x2, x3))%core in (let (a0, b0) := a in diff --git a/src/Specific/IntegrationTestMontgomeryP256_128Display.log b/src/Specific/IntegrationTestMontgomeryP256_128Display.log index 260a1ff5a..3edcd5cba 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128Display.log +++ b/src/Specific/IntegrationTestMontgomeryP256_128Display.log @@ -29,7 +29,7 @@ Interp-η uint128_t _, uint8_t x82 = addcarryx_u128(0x0, x57, x69); uint128_t x84, uint8_t x85 = addcarryx_u128(x82, x60, x75); uint128_t x87, uint8_t x88 = addcarryx_u128(x85, x63, x78); - uint8_t x89 = x88 + x64; + uint8_t x89 = (x88 + x64); uint128_t x91, uint8_t x92 = subborrow_u128(0x0, x84, 0xffffffffffffffffffffffffL); uint128_t x94, uint8_t x95 = subborrow_u128(x92, x87, 0xffffffff000000010000000000000000L); uint128_t _, uint8_t x98 = subborrow_u128(x95, x89, 0x0); diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.log b/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.log index e9a2afeb3..53c690df8 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.log +++ b/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.log @@ -2,7 +2,7 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x1, x2)%core, - uint128_t x3 = x2 | x1; + uint128_t x3 = (x2 | x1); return x3) x : word128 * word128 → ReturnType uint128_t diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.log b/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.log index 76ead3f3d..ea60d9f66 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.log +++ b/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.log @@ -5,9 +5,9 @@ Interp-η uint128_t x4, uint8_t x5 = subborrow_u128(0x0, 0x0, x2); uint128_t x7, uint8_t x8 = subborrow_u128(x5, 0x0, x1); uint128_t x9 = (uint128_t)cmovznz(x8, 0x0, 0xffffffffffffffffffffffffffffffffL); - uint128_t x10 = x9 & 0xffffffffffffffffffffffffL; + uint128_t x10 = (x9 & 0xffffffffffffffffffffffffL); uint128_t x12, uint8_t x13 = addcarryx_u128(0x0, x4, x10); - uint128_t x14 = x9 & 0xffffffff000000010000000000000000L; + uint128_t x14 = (x9 & 0xffffffff000000010000000000000000L); uint128_t x16, uint8_t _ = addcarryx_u128(x13, x7, x14); (Return x16, Return x12)) x diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.log b/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.log index 39885afbc..70f224d33 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.log +++ b/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.log @@ -5,9 +5,9 @@ Interp-η uint128_t x9, uint8_t x10 = subborrow_u128(0x0, x5, x7); uint128_t x12, uint8_t x13 = subborrow_u128(x10, x4, x6); uint128_t x14 = (uint128_t)cmovznz(x13, 0x0, 0xffffffffffffffffffffffffffffffffL); - uint128_t x15 = x14 & 0xffffffffffffffffffffffffL; + uint128_t x15 = (x14 & 0xffffffffffffffffffffffffL); uint128_t x17, uint8_t x18 = addcarryx_u128(0x0, x9, x15); - uint128_t x19 = x14 & 0xffffffff000000010000000000000000L; + uint128_t x19 = (x14 & 0xffffffff000000010000000000000000L); uint128_t x21, uint8_t _ = addcarryx_u128(x18, x12, x19); (Return x21, Return x17)) (x, x0)%core diff --git a/src/Specific/IntegrationTestSubDisplay.log b/src/Specific/IntegrationTestSubDisplay.log index ae675b0e7..cbb1c6ff5 100644 --- a/src/Specific/IntegrationTestSubDisplay.log +++ b/src/Specific/IntegrationTestSubDisplay.log @@ -2,31 +2,31 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core, - uint64_t x20 = 0xffffffffffffe + x10 - x18; - uint64_t x21 = 0xffffffffffffe + x11 - x19; - uint64_t x22 = 0xffffffffffffe + x9 - x17; - uint64_t x23 = 0xffffffffffffe + x7 - x15; - uint64_t x24 = 0xfffffffffffda + x5 - x13; - uint64_t x25 = x24 >> 0x33; - uint64_t x26 = x24 & 0x7ffffffffffff; - uint64_t x27 = x25 + x23; - uint64_t x28 = x27 >> 0x33; - uint64_t x29 = x27 & 0x7ffffffffffff; - uint64_t x30 = x28 + x22; - uint64_t x31 = x30 >> 0x33; - uint64_t x32 = x30 & 0x7ffffffffffff; - uint64_t x33 = x31 + x21; - uint64_t x34 = x33 >> 0x33; - uint64_t x35 = x33 & 0x7ffffffffffff; - uint64_t x36 = x34 + x20; - uint64_t x37 = x36 >> 0x33; - uint64_t x38 = x36 & 0x7ffffffffffff; - uint64_t x39 = x26 + 0x13 * x37; - uint64_t x40 = x39 >> 0x33; - uint64_t x41 = x39 & 0x7ffffffffffff; - uint64_t x42 = x40 + x29; - uint64_t x43 = x42 >> 0x33; - uint64_t x44 = x42 & 0x7ffffffffffff; - return (Return x38, Return x35, x43 + x32, Return x44, Return x41)) + uint64_t x20 = ((0xffffffffffffe + x10) - x18); + uint64_t x21 = ((0xffffffffffffe + x11) - x19); + uint64_t x22 = ((0xffffffffffffe + x9) - x17); + uint64_t x23 = ((0xffffffffffffe + x7) - x15); + uint64_t x24 = ((0xfffffffffffda + x5) - x13); + uint64_t x25 = (x24 >> 0x33); + uint64_t x26 = (x24 & 0x7ffffffffffff); + uint64_t x27 = (x25 + x23); + uint64_t x28 = (x27 >> 0x33); + uint64_t x29 = (x27 & 0x7ffffffffffff); + uint64_t x30 = (x28 + x22); + uint64_t x31 = (x30 >> 0x33); + uint64_t x32 = (x30 & 0x7ffffffffffff); + uint64_t x33 = (x31 + x21); + uint64_t x34 = (x33 >> 0x33); + uint64_t x35 = (x33 & 0x7ffffffffffff); + uint64_t x36 = (x34 + x20); + uint64_t x37 = (x36 >> 0x33); + uint64_t x38 = (x36 & 0x7ffffffffffff); + uint64_t x39 = (x26 + (0x13 * x37)); + uint64_t x40 = (x39 >> 0x33); + uint64_t x41 = (x39 & 0x7ffffffffffff); + uint64_t x42 = (x40 + x29); + uint64_t x43 = (x42 >> 0x33); + uint64_t x44 = (x42 & 0x7ffffffffffff); + return (Return x38, Return x35, (x43 + x32), Return x44, Return x41)) (x, x0)%core : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/NISTP256/AMD64/femulDisplay.log b/src/Specific/NISTP256/AMD64/femulDisplay.log index 982d44aaf..78afa86fa 100644 --- a/src/Specific/NISTP256/AMD64/femulDisplay.log +++ b/src/Specific/NISTP256/AMD64/femulDisplay.log @@ -47,7 +47,7 @@ Interp-η uint64_t x143, uint8_t x144 = addcarryx_u64(x141, x107, x128); uint64_t x146, uint8_t x147 = addcarryx_u64(x144, x110, x131); uint64_t x149, uint8_t x150 = addcarryx_u64(x147, x113, x134); - uint8_t x151 = x150 + x114; + uint8_t x151 = (x150 + x114); uint64_t x153, uint64_t x154 = mulx_u64(x9, x11); uint64_t x156, uint64_t x157 = mulx_u64(x9, x13); uint64_t x159, uint64_t x160 = mulx_u64(x9, x15); @@ -73,7 +73,7 @@ Interp-η uint64_t x219, uint8_t x220 = addcarryx_u64(x217, x183, x204); uint64_t x222, uint8_t x223 = addcarryx_u64(x220, x186, x207); uint64_t x225, uint8_t x226 = addcarryx_u64(x223, x189, x210); - uint8_t x227 = x226 + x190; + uint8_t x227 = (x226 + x190); uint64_t x229, uint64_t x230 = mulx_u64(x8, x11); uint64_t x232, uint64_t x233 = mulx_u64(x8, x13); uint64_t x235, uint64_t x236 = mulx_u64(x8, x15); @@ -99,7 +99,7 @@ Interp-η uint64_t x295, uint8_t x296 = addcarryx_u64(x293, x259, x280); uint64_t x298, uint8_t x299 = addcarryx_u64(x296, x262, x283); uint64_t x301, uint8_t x302 = addcarryx_u64(x299, x265, x286); - uint8_t x303 = x302 + x266; + uint8_t x303 = (x302 + x266); uint64_t x305, uint8_t x306 = subborrow_u64(0x0, x292, 0xffffffffffffffffL); uint64_t x308, uint8_t x309 = subborrow_u64(x306, x295, 0xffffffff); uint64_t x311, uint8_t x312 = subborrow_u64(x309, x298, 0x0); diff --git a/src/Specific/NISTP256/AMD64/fenzDisplay.log b/src/Specific/NISTP256/AMD64/fenzDisplay.log index 399df24d4..65afbc2d6 100644 --- a/src/Specific/NISTP256/AMD64/fenzDisplay.log +++ b/src/Specific/NISTP256/AMD64/fenzDisplay.log @@ -2,9 +2,9 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x5, x6, x4, x2)%core, - uint64_t x7 = x6 | x5; - uint64_t x8 = x4 | x7; - uint64_t x9 = x2 | x8; + uint64_t x7 = (x6 | x5); + uint64_t x8 = (x4 | x7); + uint64_t x9 = (x2 | x8); return x9) x : word64 * word64 * word64 * word64 → ReturnType uint64_t diff --git a/src/Specific/NISTP256/AMD64/feoppDisplay.log b/src/Specific/NISTP256/AMD64/feoppDisplay.log index 211b2b863..87297dfac 100644 --- a/src/Specific/NISTP256/AMD64/feoppDisplay.log +++ b/src/Specific/NISTP256/AMD64/feoppDisplay.log @@ -7,12 +7,12 @@ Interp-η uint64_t x14, uint8_t x15 = subborrow_u64(x12, 0x0, x6); uint64_t x17, uint8_t x18 = subborrow_u64(x15, 0x0, x5); uint64_t x19 = (uint64_t)cmovznz(x18, 0x0, 0xffffffffffffffffL); - uint64_t x20 = x19 & 0xffffffffffffffffL; + uint64_t x20 = (x19 & 0xffffffffffffffffL); uint64_t x22, uint8_t x23 = addcarryx_u64(0x0, x8, x20); - uint64_t x24 = x19 & 0xffffffff; + uint64_t x24 = (x19 & 0xffffffff); uint64_t x26, uint8_t x27 = addcarryx_u64(x23, x11, x24); uint64_t x29, uint8_t x30 = addcarryx_u64(x27, x14, 0x0); - uint64_t x31 = x19 & 0xffffffff00000001L; + uint64_t x31 = (x19 & 0xffffffff00000001L); uint64_t x33, uint8_t _ = addcarryx_u64(x30, x17, x31); (Return x33, Return x29, Return x26, Return x22)) x diff --git a/src/Specific/NISTP256/AMD64/fesubDisplay.log b/src/Specific/NISTP256/AMD64/fesubDisplay.log index eb4289fd2..410fead3f 100644 --- a/src/Specific/NISTP256/AMD64/fesubDisplay.log +++ b/src/Specific/NISTP256/AMD64/fesubDisplay.log @@ -7,12 +7,12 @@ Interp-η uint64_t x23, uint8_t x24 = subborrow_u64(x21, x9, x15); uint64_t x26, uint8_t x27 = subborrow_u64(x24, x8, x14); uint64_t x28 = (uint64_t)cmovznz(x27, 0x0, 0xffffffffffffffffL); - uint64_t x29 = x28 & 0xffffffffffffffffL; + uint64_t x29 = (x28 & 0xffffffffffffffffL); uint64_t x31, uint8_t x32 = addcarryx_u64(0x0, x17, x29); - uint64_t x33 = x28 & 0xffffffff; + uint64_t x33 = (x28 & 0xffffffff); uint64_t x35, uint8_t x36 = addcarryx_u64(x32, x20, x33); uint64_t x38, uint8_t x39 = addcarryx_u64(x36, x23, 0x0); - uint64_t x40 = x28 & 0xffffffff00000001L; + uint64_t x40 = (x28 & 0xffffffff00000001L); uint64_t x42, uint8_t _ = addcarryx_u64(x39, x26, x40); (Return x42, Return x38, Return x35, Return x31)) (x, x0)%core diff --git a/src/Specific/X25519/C32/femulDisplay.log b/src/Specific/X25519/C32/femulDisplay.log index 12fa54d8a..7564ec007 100644 --- a/src/Specific/X25519/C32/femulDisplay.log +++ b/src/Specific/X25519/C32/femulDisplay.log @@ -2,87 +2,87 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core, - uint64_t x40 = (uint64_t) x23 * x5; - uint64_t x41 = (uint64_t) x23 * x7 + (uint64_t) x25 * x5; - uint64_t x42 = (uint64_t) (0x2 * x25) * x7 + (uint64_t) x23 * x9 + (uint64_t) x27 * x5; - uint64_t x43 = (uint64_t) x25 * x9 + (uint64_t) x27 * x7 + (uint64_t) x23 * x11 + (uint64_t) x29 * x5; - uint64_t x44 = (uint64_t) x27 * x9 + 0x2 * ((uint64_t) x25 * x11 + (uint64_t) x29 * x7) + (uint64_t) x23 * x13 + (uint64_t) x31 * x5; - uint64_t x45 = (uint64_t) x27 * x11 + (uint64_t) x29 * x9 + (uint64_t) x25 * x13 + (uint64_t) x31 * x7 + (uint64_t) x23 * x15 + (uint64_t) x33 * x5; - uint64_t x46 = 0x2 * ((uint64_t) x29 * x11 + (uint64_t) x25 * x15 + (uint64_t) x33 * x7) + (uint64_t) x27 * x13 + (uint64_t) x31 * x9 + (uint64_t) x23 * x17 + (uint64_t) x35 * x5; - uint64_t x47 = (uint64_t) x29 * x13 + (uint64_t) x31 * x11 + (uint64_t) x27 * x15 + (uint64_t) x33 * x9 + (uint64_t) x25 * x17 + (uint64_t) x35 * x7 + (uint64_t) x23 * x19 + (uint64_t) x37 * x5; - uint64_t x48 = (uint64_t) x31 * x13 + 0x2 * ((uint64_t) x29 * x15 + (uint64_t) x33 * x11 + (uint64_t) x25 * x19 + (uint64_t) x37 * x7) + (uint64_t) x27 * x17 + (uint64_t) x35 * x9 + (uint64_t) x23 * x21 + (uint64_t) x39 * x5; - uint64_t x49 = (uint64_t) x31 * x15 + (uint64_t) x33 * x13 + (uint64_t) x29 * x17 + (uint64_t) x35 * x11 + (uint64_t) x27 * x19 + (uint64_t) x37 * x9 + (uint64_t) x25 * x21 + (uint64_t) x39 * x7 + (uint64_t) x23 * x20 + (uint64_t) x38 * x5; - uint64_t x50 = 0x2 * ((uint64_t) x33 * x15 + (uint64_t) x29 * x19 + (uint64_t) x37 * x11 + (uint64_t) x25 * x20 + (uint64_t) x38 * x7) + (uint64_t) x31 * x17 + (uint64_t) x35 * x13 + (uint64_t) x27 * x21 + (uint64_t) x39 * x9; - uint64_t x51 = (uint64_t) x33 * x17 + (uint64_t) x35 * x15 + (uint64_t) x31 * x19 + (uint64_t) x37 * x13 + (uint64_t) x29 * x21 + (uint64_t) x39 * x11 + (uint64_t) x27 * x20 + (uint64_t) x38 * x9; - uint64_t x52 = (uint64_t) x35 * x17 + 0x2 * ((uint64_t) x33 * x19 + (uint64_t) x37 * x15 + (uint64_t) x29 * x20 + (uint64_t) x38 * x11) + (uint64_t) x31 * x21 + (uint64_t) x39 * x13; - uint64_t x53 = (uint64_t) x35 * x19 + (uint64_t) x37 * x17 + (uint64_t) x33 * x21 + (uint64_t) x39 * x15 + (uint64_t) x31 * x20 + (uint64_t) x38 * x13; - uint64_t x54 = 0x2 * ((uint64_t) x37 * x19 + (uint64_t) x33 * x20 + (uint64_t) x38 * x15) + (uint64_t) x35 * x21 + (uint64_t) x39 * x17; - uint64_t x55 = (uint64_t) x37 * x21 + (uint64_t) x39 * x19 + (uint64_t) x35 * x20 + (uint64_t) x38 * x17; - uint64_t x56 = (uint64_t) x39 * x21 + 0x2 * ((uint64_t) x37 * x20 + (uint64_t) x38 * x19); - uint64_t x57 = (uint64_t) x39 * x20 + (uint64_t) x38 * x21; - uint64_t x58 = (uint64_t) (0x2 * x38) * x20; - uint64_t x59 = x48 + x58 << 0x4; - uint64_t x60 = x59 + x58 << 0x1; - uint64_t x61 = x60 + x58; - uint64_t x62 = x47 + x57 << 0x4; - uint64_t x63 = x62 + x57 << 0x1; - uint64_t x64 = x63 + x57; - uint64_t x65 = x46 + x56 << 0x4; - uint64_t x66 = x65 + x56 << 0x1; - uint64_t x67 = x66 + x56; - uint64_t x68 = x45 + x55 << 0x4; - uint64_t x69 = x68 + x55 << 0x1; - uint64_t x70 = x69 + x55; - uint64_t x71 = x44 + x54 << 0x4; - uint64_t x72 = x71 + x54 << 0x1; - uint64_t x73 = x72 + x54; - uint64_t x74 = x43 + x53 << 0x4; - uint64_t x75 = x74 + x53 << 0x1; - uint64_t x76 = x75 + x53; - uint64_t x77 = x42 + x52 << 0x4; - uint64_t x78 = x77 + x52 << 0x1; - uint64_t x79 = x78 + x52; - uint64_t x80 = x41 + x51 << 0x4; - uint64_t x81 = x80 + x51 << 0x1; - uint64_t x82 = x81 + x51; - uint64_t x83 = x40 + x50 << 0x4; - uint64_t x84 = x83 + x50 << 0x1; - uint64_t x85 = x84 + x50; - uint64_t x86 = x85 >> 0x1a; - uint32_t x87 = (uint32_t) x85 & 0x3ffffff; - uint64_t x88 = x86 + x82; - uint64_t x89 = x88 >> 0x19; - uint32_t x90 = (uint32_t) x88 & 0x1ffffff; - uint64_t x91 = x89 + x79; - uint64_t x92 = x91 >> 0x1a; - uint32_t x93 = (uint32_t) x91 & 0x3ffffff; - uint64_t x94 = x92 + x76; - uint64_t x95 = x94 >> 0x19; - uint32_t x96 = (uint32_t) x94 & 0x1ffffff; - uint64_t x97 = x95 + x73; - uint64_t x98 = x97 >> 0x1a; - uint32_t x99 = (uint32_t) x97 & 0x3ffffff; - uint64_t x100 = x98 + x70; - uint64_t x101 = x100 >> 0x19; - uint32_t x102 = (uint32_t) x100 & 0x1ffffff; - uint64_t x103 = x101 + x67; + uint64_t x40 = ((uint64_t)x23 * x5); + uint64_t x41 = (((uint64_t)x23 * x7) + ((uint64_t)x25 * x5)); + uint64_t x42 = ((((uint64_t)(0x2 * x25) * x7) + ((uint64_t)x23 * x9)) + ((uint64_t)x27 * x5)); + uint64_t x43 = (((((uint64_t)x25 * x9) + ((uint64_t)x27 * x7)) + ((uint64_t)x23 * x11)) + ((uint64_t)x29 * x5)); + uint64_t x44 = (((((uint64_t)x27 * x9) + (0x2 * (((uint64_t)x25 * x11) + ((uint64_t)x29 * x7)))) + ((uint64_t)x23 * x13)) + ((uint64_t)x31 * x5)); + uint64_t x45 = (((((((uint64_t)x27 * x11) + ((uint64_t)x29 * x9)) + ((uint64_t)x25 * x13)) + ((uint64_t)x31 * x7)) + ((uint64_t)x23 * x15)) + ((uint64_t)x33 * x5)); + uint64_t x46 = (((((0x2 * ((((uint64_t)x29 * x11) + ((uint64_t)x25 * x15)) + ((uint64_t)x33 * x7))) + ((uint64_t)x27 * x13)) + ((uint64_t)x31 * x9)) + ((uint64_t)x23 * x17)) + ((uint64_t)x35 * x5)); + uint64_t x47 = (((((((((uint64_t)x29 * x13) + ((uint64_t)x31 * x11)) + ((uint64_t)x27 * x15)) + ((uint64_t)x33 * x9)) + ((uint64_t)x25 * x17)) + ((uint64_t)x35 * x7)) + ((uint64_t)x23 * x19)) + ((uint64_t)x37 * x5)); + uint64_t x48 = (((((((uint64_t)x31 * x13) + (0x2 * (((((uint64_t)x29 * x15) + ((uint64_t)x33 * x11)) + ((uint64_t)x25 * x19)) + ((uint64_t)x37 * x7)))) + ((uint64_t)x27 * x17)) + ((uint64_t)x35 * x9)) + ((uint64_t)x23 * x21)) + ((uint64_t)x39 * x5)); + uint64_t x49 = (((((((((((uint64_t)x31 * x15) + ((uint64_t)x33 * x13)) + ((uint64_t)x29 * x17)) + ((uint64_t)x35 * x11)) + ((uint64_t)x27 * x19)) + ((uint64_t)x37 * x9)) + ((uint64_t)x25 * x21)) + ((uint64_t)x39 * x7)) + ((uint64_t)x23 * x20)) + ((uint64_t)x38 * x5)); + uint64_t x50 = (((((0x2 * ((((((uint64_t)x33 * x15) + ((uint64_t)x29 * x19)) + ((uint64_t)x37 * x11)) + ((uint64_t)x25 * x20)) + ((uint64_t)x38 * x7))) + ((uint64_t)x31 * x17)) + ((uint64_t)x35 * x13)) + ((uint64_t)x27 * x21)) + ((uint64_t)x39 * x9)); + uint64_t x51 = (((((((((uint64_t)x33 * x17) + ((uint64_t)x35 * x15)) + ((uint64_t)x31 * x19)) + ((uint64_t)x37 * x13)) + ((uint64_t)x29 * x21)) + ((uint64_t)x39 * x11)) + ((uint64_t)x27 * x20)) + ((uint64_t)x38 * x9)); + uint64_t x52 = (((((uint64_t)x35 * x17) + (0x2 * (((((uint64_t)x33 * x19) + ((uint64_t)x37 * x15)) + ((uint64_t)x29 * x20)) + ((uint64_t)x38 * x11)))) + ((uint64_t)x31 * x21)) + ((uint64_t)x39 * x13)); + uint64_t x53 = (((((((uint64_t)x35 * x19) + ((uint64_t)x37 * x17)) + ((uint64_t)x33 * x21)) + ((uint64_t)x39 * x15)) + ((uint64_t)x31 * x20)) + ((uint64_t)x38 * x13)); + uint64_t x54 = (((0x2 * ((((uint64_t)x37 * x19) + ((uint64_t)x33 * x20)) + ((uint64_t)x38 * x15))) + ((uint64_t)x35 * x21)) + ((uint64_t)x39 * x17)); + uint64_t x55 = (((((uint64_t)x37 * x21) + ((uint64_t)x39 * x19)) + ((uint64_t)x35 * x20)) + ((uint64_t)x38 * x17)); + uint64_t x56 = (((uint64_t)x39 * x21) + (0x2 * (((uint64_t)x37 * x20) + ((uint64_t)x38 * x19)))); + uint64_t x57 = (((uint64_t)x39 * x20) + ((uint64_t)x38 * x21)); + uint64_t x58 = ((uint64_t)(0x2 * x38) * x20); + uint64_t x59 = (x48 + (x58 << 0x4)); + uint64_t x60 = (x59 + (x58 << 0x1)); + uint64_t x61 = (x60 + x58); + uint64_t x62 = (x47 + (x57 << 0x4)); + uint64_t x63 = (x62 + (x57 << 0x1)); + uint64_t x64 = (x63 + x57); + uint64_t x65 = (x46 + (x56 << 0x4)); + uint64_t x66 = (x65 + (x56 << 0x1)); + uint64_t x67 = (x66 + x56); + uint64_t x68 = (x45 + (x55 << 0x4)); + uint64_t x69 = (x68 + (x55 << 0x1)); + uint64_t x70 = (x69 + x55); + uint64_t x71 = (x44 + (x54 << 0x4)); + uint64_t x72 = (x71 + (x54 << 0x1)); + uint64_t x73 = (x72 + x54); + uint64_t x74 = (x43 + (x53 << 0x4)); + uint64_t x75 = (x74 + (x53 << 0x1)); + uint64_t x76 = (x75 + x53); + uint64_t x77 = (x42 + (x52 << 0x4)); + uint64_t x78 = (x77 + (x52 << 0x1)); + uint64_t x79 = (x78 + x52); + uint64_t x80 = (x41 + (x51 << 0x4)); + uint64_t x81 = (x80 + (x51 << 0x1)); + uint64_t x82 = (x81 + x51); + uint64_t x83 = (x40 + (x50 << 0x4)); + uint64_t x84 = (x83 + (x50 << 0x1)); + uint64_t x85 = (x84 + x50); + uint64_t x86 = (x85 >> 0x1a); + uint32_t x87 = ((uint32_t)x85 & 0x3ffffff); + uint64_t x88 = (x86 + x82); + uint64_t x89 = (x88 >> 0x19); + uint32_t x90 = ((uint32_t)x88 & 0x1ffffff); + uint64_t x91 = (x89 + x79); + uint64_t x92 = (x91 >> 0x1a); + uint32_t x93 = ((uint32_t)x91 & 0x3ffffff); + uint64_t x94 = (x92 + x76); + uint64_t x95 = (x94 >> 0x19); + uint32_t x96 = ((uint32_t)x94 & 0x1ffffff); + uint64_t x97 = (x95 + x73); + uint64_t x98 = (x97 >> 0x1a); + uint32_t x99 = ((uint32_t)x97 & 0x3ffffff); + uint64_t x100 = (x98 + x70); + uint64_t x101 = (x100 >> 0x19); + uint32_t x102 = ((uint32_t)x100 & 0x1ffffff); + uint64_t x103 = (x101 + x67); uint32_t x104 = (uint32_t) (x103 >> 0x1a); - uint32_t x105 = (uint32_t) x103 & 0x3ffffff; - uint64_t x106 = x104 + x64; + uint32_t x105 = ((uint32_t)x103 & 0x3ffffff); + uint64_t x106 = (x104 + x64); uint32_t x107 = (uint32_t) (x106 >> 0x19); - uint32_t x108 = (uint32_t) x106 & 0x1ffffff; - uint64_t x109 = x107 + x61; + uint32_t x108 = ((uint32_t)x106 & 0x1ffffff); + uint64_t x109 = (x107 + x61); uint32_t x110 = (uint32_t) (x109 >> 0x1a); - uint32_t x111 = (uint32_t) x109 & 0x3ffffff; - uint64_t x112 = x110 + x49; + uint32_t x111 = ((uint32_t)x109 & 0x3ffffff); + uint64_t x112 = (x110 + x49); uint32_t x113 = (uint32_t) (x112 >> 0x19); - uint32_t x114 = (uint32_t) x112 & 0x1ffffff; - uint64_t x115 = x87 + (uint64_t) 0x13 * x113; + uint32_t x114 = ((uint32_t)x112 & 0x1ffffff); + uint64_t x115 = (x87 + ((uint64_t)0x13 * x113)); uint32_t x116 = (uint32_t) (x115 >> 0x1a); - uint32_t x117 = (uint32_t) x115 & 0x3ffffff; - uint32_t x118 = x116 + x90; - uint32_t x119 = x118 >> 0x19; - uint32_t x120 = x118 & 0x1ffffff; - return (Return x114, Return x111, Return x108, Return x105, Return x102, Return x99, Return x96, x119 + x93, Return x120, Return x117)) + uint32_t x117 = ((uint32_t)x115 & 0x3ffffff); + uint32_t x118 = (x116 + x90); + uint32_t x119 = (x118 >> 0x19); + uint32_t x120 = (x118 & 0x1ffffff); + return (Return x114, Return x111, Return x108, Return x105, Return x102, Return x99, Return x96, (x119 + x93), Return x120, Return x117)) (x, x0)%core : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) diff --git a/src/Specific/X25519/C32/fesquareDisplay.log b/src/Specific/X25519/C32/fesquareDisplay.log index d9b0c533f..dc270a356 100644 --- a/src/Specific/X25519/C32/fesquareDisplay.log +++ b/src/Specific/X25519/C32/fesquareDisplay.log @@ -2,87 +2,87 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x17, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core, - uint64_t x19 = (uint64_t) x2 * x2; - uint64_t x20 = (uint64_t) (0x2 * x2) * x4; - uint64_t x21 = 0x2 * ((uint64_t) x4 * x4 + (uint64_t) x2 * x6); - uint64_t x22 = 0x2 * ((uint64_t) x4 * x6 + (uint64_t) x2 * x8); - uint64_t x23 = (uint64_t) x6 * x6 + (uint64_t) (0x4 * x4) * x8 + (uint64_t) (0x2 * x2) * x10; - uint64_t x24 = 0x2 * ((uint64_t) x6 * x8 + (uint64_t) x4 * x10 + (uint64_t) x2 * x12); - uint64_t x25 = 0x2 * ((uint64_t) x8 * x8 + (uint64_t) x6 * x10 + (uint64_t) x2 * x14 + (uint64_t) (0x2 * x4) * x12); - uint64_t x26 = 0x2 * ((uint64_t) x8 * x10 + (uint64_t) x6 * x12 + (uint64_t) x4 * x14 + (uint64_t) x2 * x16); - uint64_t x27 = (uint64_t) x10 * x10 + 0x2 * ((uint64_t) x6 * x14 + (uint64_t) x2 * x18 + 0x2 * ((uint64_t) x4 * x16 + (uint64_t) x8 * x12)); - uint64_t x28 = 0x2 * ((uint64_t) x10 * x12 + (uint64_t) x8 * x14 + (uint64_t) x6 * x16 + (uint64_t) x4 * x18 + (uint64_t) x2 * x17); - uint64_t x29 = 0x2 * ((uint64_t) x12 * x12 + (uint64_t) x10 * x14 + (uint64_t) x6 * x18 + 0x2 * ((uint64_t) x8 * x16 + (uint64_t) x4 * x17)); - uint64_t x30 = 0x2 * ((uint64_t) x12 * x14 + (uint64_t) x10 * x16 + (uint64_t) x8 * x18 + (uint64_t) x6 * x17); - uint64_t x31 = (uint64_t) x14 * x14 + 0x2 * ((uint64_t) x10 * x18 + 0x2 * ((uint64_t) x12 * x16 + (uint64_t) x8 * x17)); - uint64_t x32 = 0x2 * ((uint64_t) x14 * x16 + (uint64_t) x12 * x18 + (uint64_t) x10 * x17); - uint64_t x33 = 0x2 * ((uint64_t) x16 * x16 + (uint64_t) x14 * x18 + (uint64_t) (0x2 * x12) * x17); - uint64_t x34 = 0x2 * ((uint64_t) x16 * x18 + (uint64_t) x14 * x17); - uint64_t x35 = (uint64_t) x18 * x18 + (uint64_t) (0x4 * x16) * x17; - uint64_t x36 = (uint64_t) (0x2 * x18) * x17; - uint64_t x37 = (uint64_t) (0x2 * x17) * x17; - uint64_t x38 = x27 + x37 << 0x4; - uint64_t x39 = x38 + x37 << 0x1; - uint64_t x40 = x39 + x37; - uint64_t x41 = x26 + x36 << 0x4; - uint64_t x42 = x41 + x36 << 0x1; - uint64_t x43 = x42 + x36; - uint64_t x44 = x25 + x35 << 0x4; - uint64_t x45 = x44 + x35 << 0x1; - uint64_t x46 = x45 + x35; - uint64_t x47 = x24 + x34 << 0x4; - uint64_t x48 = x47 + x34 << 0x1; - uint64_t x49 = x48 + x34; - uint64_t x50 = x23 + x33 << 0x4; - uint64_t x51 = x50 + x33 << 0x1; - uint64_t x52 = x51 + x33; - uint64_t x53 = x22 + x32 << 0x4; - uint64_t x54 = x53 + x32 << 0x1; - uint64_t x55 = x54 + x32; - uint64_t x56 = x21 + x31 << 0x4; - uint64_t x57 = x56 + x31 << 0x1; - uint64_t x58 = x57 + x31; - uint64_t x59 = x20 + x30 << 0x4; - uint64_t x60 = x59 + x30 << 0x1; - uint64_t x61 = x60 + x30; - uint64_t x62 = x19 + x29 << 0x4; - uint64_t x63 = x62 + x29 << 0x1; - uint64_t x64 = x63 + x29; - uint64_t x65 = x64 >> 0x1a; - uint32_t x66 = (uint32_t) x64 & 0x3ffffff; - uint64_t x67 = x65 + x61; - uint64_t x68 = x67 >> 0x19; - uint32_t x69 = (uint32_t) x67 & 0x1ffffff; - uint64_t x70 = x68 + x58; - uint64_t x71 = x70 >> 0x1a; - uint32_t x72 = (uint32_t) x70 & 0x3ffffff; - uint64_t x73 = x71 + x55; - uint64_t x74 = x73 >> 0x19; - uint32_t x75 = (uint32_t) x73 & 0x1ffffff; - uint64_t x76 = x74 + x52; - uint64_t x77 = x76 >> 0x1a; - uint32_t x78 = (uint32_t) x76 & 0x3ffffff; - uint64_t x79 = x77 + x49; - uint64_t x80 = x79 >> 0x19; - uint32_t x81 = (uint32_t) x79 & 0x1ffffff; - uint64_t x82 = x80 + x46; + uint64_t x19 = ((uint64_t)x2 * x2); + uint64_t x20 = ((uint64_t)(0x2 * x2) * x4); + uint64_t x21 = (0x2 * (((uint64_t)x4 * x4) + ((uint64_t)x2 * x6))); + uint64_t x22 = (0x2 * (((uint64_t)x4 * x6) + ((uint64_t)x2 * x8))); + uint64_t x23 = ((((uint64_t)x6 * x6) + ((uint64_t)(0x4 * x4) * x8)) + ((uint64_t)(0x2 * x2) * x10)); + uint64_t x24 = (0x2 * ((((uint64_t)x6 * x8) + ((uint64_t)x4 * x10)) + ((uint64_t)x2 * x12))); + uint64_t x25 = (0x2 * (((((uint64_t)x8 * x8) + ((uint64_t)x6 * x10)) + ((uint64_t)x2 * x14)) + ((uint64_t)(0x2 * x4) * x12))); + uint64_t x26 = (0x2 * (((((uint64_t)x8 * x10) + ((uint64_t)x6 * x12)) + ((uint64_t)x4 * x14)) + ((uint64_t)x2 * x16))); + uint64_t x27 = (((uint64_t)x10 * x10) + (0x2 * ((((uint64_t)x6 * x14) + ((uint64_t)x2 * x18)) + (0x2 * (((uint64_t)x4 * x16) + ((uint64_t)x8 * x12)))))); + uint64_t x28 = (0x2 * ((((((uint64_t)x10 * x12) + ((uint64_t)x8 * x14)) + ((uint64_t)x6 * x16)) + ((uint64_t)x4 * x18)) + ((uint64_t)x2 * x17))); + uint64_t x29 = (0x2 * (((((uint64_t)x12 * x12) + ((uint64_t)x10 * x14)) + ((uint64_t)x6 * x18)) + (0x2 * (((uint64_t)x8 * x16) + ((uint64_t)x4 * x17))))); + uint64_t x30 = (0x2 * (((((uint64_t)x12 * x14) + ((uint64_t)x10 * x16)) + ((uint64_t)x8 * x18)) + ((uint64_t)x6 * x17))); + uint64_t x31 = (((uint64_t)x14 * x14) + (0x2 * (((uint64_t)x10 * x18) + (0x2 * (((uint64_t)x12 * x16) + ((uint64_t)x8 * x17)))))); + uint64_t x32 = (0x2 * ((((uint64_t)x14 * x16) + ((uint64_t)x12 * x18)) + ((uint64_t)x10 * x17))); + uint64_t x33 = (0x2 * ((((uint64_t)x16 * x16) + ((uint64_t)x14 * x18)) + ((uint64_t)(0x2 * x12) * x17))); + uint64_t x34 = (0x2 * (((uint64_t)x16 * x18) + ((uint64_t)x14 * x17))); + uint64_t x35 = (((uint64_t)x18 * x18) + ((uint64_t)(0x4 * x16) * x17)); + uint64_t x36 = ((uint64_t)(0x2 * x18) * x17); + uint64_t x37 = ((uint64_t)(0x2 * x17) * x17); + uint64_t x38 = (x27 + (x37 << 0x4)); + uint64_t x39 = (x38 + (x37 << 0x1)); + uint64_t x40 = (x39 + x37); + uint64_t x41 = (x26 + (x36 << 0x4)); + uint64_t x42 = (x41 + (x36 << 0x1)); + uint64_t x43 = (x42 + x36); + uint64_t x44 = (x25 + (x35 << 0x4)); + uint64_t x45 = (x44 + (x35 << 0x1)); + uint64_t x46 = (x45 + x35); + uint64_t x47 = (x24 + (x34 << 0x4)); + uint64_t x48 = (x47 + (x34 << 0x1)); + uint64_t x49 = (x48 + x34); + uint64_t x50 = (x23 + (x33 << 0x4)); + uint64_t x51 = (x50 + (x33 << 0x1)); + uint64_t x52 = (x51 + x33); + uint64_t x53 = (x22 + (x32 << 0x4)); + uint64_t x54 = (x53 + (x32 << 0x1)); + uint64_t x55 = (x54 + x32); + uint64_t x56 = (x21 + (x31 << 0x4)); + uint64_t x57 = (x56 + (x31 << 0x1)); + uint64_t x58 = (x57 + x31); + uint64_t x59 = (x20 + (x30 << 0x4)); + uint64_t x60 = (x59 + (x30 << 0x1)); + uint64_t x61 = (x60 + x30); + uint64_t x62 = (x19 + (x29 << 0x4)); + uint64_t x63 = (x62 + (x29 << 0x1)); + uint64_t x64 = (x63 + x29); + uint64_t x65 = (x64 >> 0x1a); + uint32_t x66 = ((uint32_t)x64 & 0x3ffffff); + uint64_t x67 = (x65 + x61); + uint64_t x68 = (x67 >> 0x19); + uint32_t x69 = ((uint32_t)x67 & 0x1ffffff); + uint64_t x70 = (x68 + x58); + uint64_t x71 = (x70 >> 0x1a); + uint32_t x72 = ((uint32_t)x70 & 0x3ffffff); + uint64_t x73 = (x71 + x55); + uint64_t x74 = (x73 >> 0x19); + uint32_t x75 = ((uint32_t)x73 & 0x1ffffff); + uint64_t x76 = (x74 + x52); + uint64_t x77 = (x76 >> 0x1a); + uint32_t x78 = ((uint32_t)x76 & 0x3ffffff); + uint64_t x79 = (x77 + x49); + uint64_t x80 = (x79 >> 0x19); + uint32_t x81 = ((uint32_t)x79 & 0x1ffffff); + uint64_t x82 = (x80 + x46); uint32_t x83 = (uint32_t) (x82 >> 0x1a); - uint32_t x84 = (uint32_t) x82 & 0x3ffffff; - uint64_t x85 = x83 + x43; + uint32_t x84 = ((uint32_t)x82 & 0x3ffffff); + uint64_t x85 = (x83 + x43); uint32_t x86 = (uint32_t) (x85 >> 0x19); - uint32_t x87 = (uint32_t) x85 & 0x1ffffff; - uint64_t x88 = x86 + x40; + uint32_t x87 = ((uint32_t)x85 & 0x1ffffff); + uint64_t x88 = (x86 + x40); uint32_t x89 = (uint32_t) (x88 >> 0x1a); - uint32_t x90 = (uint32_t) x88 & 0x3ffffff; - uint64_t x91 = x89 + x28; + uint32_t x90 = ((uint32_t)x88 & 0x3ffffff); + uint64_t x91 = (x89 + x28); uint32_t x92 = (uint32_t) (x91 >> 0x19); - uint32_t x93 = (uint32_t) x91 & 0x1ffffff; - uint64_t x94 = x66 + (uint64_t) 0x13 * x92; + uint32_t x93 = ((uint32_t)x91 & 0x1ffffff); + uint64_t x94 = (x66 + ((uint64_t)0x13 * x92)); uint32_t x95 = (uint32_t) (x94 >> 0x1a); - uint32_t x96 = (uint32_t) x94 & 0x3ffffff; - uint32_t x97 = x95 + x69; - uint32_t x98 = x97 >> 0x19; - uint32_t x99 = x97 & 0x1ffffff; - return (Return x93, Return x90, Return x87, Return x84, Return x81, Return x78, Return x75, x98 + x72, Return x99, Return x96)) + uint32_t x96 = ((uint32_t)x94 & 0x3ffffff); + uint32_t x97 = (x95 + x69); + uint32_t x98 = (x97 >> 0x19); + uint32_t x99 = (x97 & 0x1ffffff); + return (Return x93, Return x90, Return x87, Return x84, Return x81, Return x78, Return x75, (x98 + x72), Return x99, Return x96)) x : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) diff --git a/src/Specific/X25519/C64/femulDisplay.log b/src/Specific/X25519/C64/femulDisplay.log index e49d7c117..6ecb01e51 100644 --- a/src/Specific/X25519/C64/femulDisplay.log +++ b/src/Specific/X25519/C64/femulDisplay.log @@ -2,39 +2,39 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core, - uint128_t x20 = (uint128_t) x5 * x13; - uint128_t x21 = (uint128_t) x5 * x15 + (uint128_t) x7 * x13; - uint128_t x22 = (uint128_t) x5 * x17 + (uint128_t) x9 * x13 + (uint128_t) x7 * x15; - uint128_t x23 = (uint128_t) x5 * x19 + (uint128_t) x11 * x13 + (uint128_t) x7 * x17 + (uint128_t) x9 * x15; - uint128_t x24 = (uint128_t) x5 * x18 + (uint128_t) x10 * x13 + (uint128_t) x11 * x15 + (uint128_t) x7 * x19 + (uint128_t) x9 * x17; - uint64_t x25 = x10 * 0x13; - uint64_t x26 = x7 * 0x13; - uint64_t x27 = x9 * 0x13; - uint64_t x28 = x11 * 0x13; - uint128_t x29 = x20 + (uint128_t) x25 * x15 + (uint128_t) x26 * x18 + (uint128_t) x27 * x19 + (uint128_t) x28 * x17; - uint128_t x30 = x21 + (uint128_t) x25 * x17 + (uint128_t) x27 * x18 + (uint128_t) x28 * x19; - uint128_t x31 = x22 + (uint128_t) x25 * x19 + (uint128_t) x28 * x18; - uint128_t x32 = x23 + (uint128_t) x25 * x18; + uint128_t x20 = ((uint128_t)x5 * x13); + uint128_t x21 = (((uint128_t)x5 * x15) + ((uint128_t)x7 * x13)); + uint128_t x22 = ((((uint128_t)x5 * x17) + ((uint128_t)x9 * x13)) + ((uint128_t)x7 * x15)); + uint128_t x23 = (((((uint128_t)x5 * x19) + ((uint128_t)x11 * x13)) + ((uint128_t)x7 * x17)) + ((uint128_t)x9 * x15)); + uint128_t x24 = ((((((uint128_t)x5 * x18) + ((uint128_t)x10 * x13)) + ((uint128_t)x11 * x15)) + ((uint128_t)x7 * x19)) + ((uint128_t)x9 * x17)); + uint64_t x25 = (x10 * 0x13); + uint64_t x26 = (x7 * 0x13); + uint64_t x27 = (x9 * 0x13); + uint64_t x28 = (x11 * 0x13); + uint128_t x29 = ((((x20 + ((uint128_t)x25 * x15)) + ((uint128_t)x26 * x18)) + ((uint128_t)x27 * x19)) + ((uint128_t)x28 * x17)); + uint128_t x30 = (((x21 + ((uint128_t)x25 * x17)) + ((uint128_t)x27 * x18)) + ((uint128_t)x28 * x19)); + uint128_t x31 = ((x22 + ((uint128_t)x25 * x19)) + ((uint128_t)x28 * x18)); + uint128_t x32 = (x23 + ((uint128_t)x25 * x18)); uint64_t x33 = (uint64_t) (x29 >> 0x33); - uint64_t x34 = (uint64_t) x29 & 0x7ffffffffffff; - uint128_t x35 = x33 + x30; + uint64_t x34 = ((uint64_t)x29 & 0x7ffffffffffff); + uint128_t x35 = (x33 + x30); uint64_t x36 = (uint64_t) (x35 >> 0x33); - uint64_t x37 = (uint64_t) x35 & 0x7ffffffffffff; - uint128_t x38 = x36 + x31; + uint64_t x37 = ((uint64_t)x35 & 0x7ffffffffffff); + uint128_t x38 = (x36 + x31); uint64_t x39 = (uint64_t) (x38 >> 0x33); - uint64_t x40 = (uint64_t) x38 & 0x7ffffffffffff; - uint128_t x41 = x39 + x32; + uint64_t x40 = ((uint64_t)x38 & 0x7ffffffffffff); + uint128_t x41 = (x39 + x32); uint64_t x42 = (uint64_t) (x41 >> 0x33); - uint64_t x43 = (uint64_t) x41 & 0x7ffffffffffff; - uint128_t x44 = x42 + x24; + uint64_t x43 = ((uint64_t)x41 & 0x7ffffffffffff); + uint128_t x44 = (x42 + x24); uint64_t x45 = (uint64_t) (x44 >> 0x33); - uint64_t x46 = (uint64_t) x44 & 0x7ffffffffffff; - uint64_t x47 = x34 + 0x13 * x45; - uint64_t x48 = x47 >> 0x33; - uint64_t x49 = x47 & 0x7ffffffffffff; - uint64_t x50 = x48 + x37; - uint64_t x51 = x50 >> 0x33; - uint64_t x52 = x50 & 0x7ffffffffffff; - return (Return x46, Return x43, x51 + x40, Return x52, Return x49)) + uint64_t x46 = ((uint64_t)x44 & 0x7ffffffffffff); + uint64_t x47 = (x34 + (0x13 * x45)); + uint64_t x48 = (x47 >> 0x33); + uint64_t x49 = (x47 & 0x7ffffffffffff); + uint64_t x50 = (x48 + x37); + uint64_t x51 = (x50 >> 0x33); + uint64_t x52 = (x50 & 0x7ffffffffffff); + return (Return x46, Return x43, (x51 + x40), Return x52, Return x49)) (x, x0)%core : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/X25519/C64/fesquareDisplay.log b/src/Specific/X25519/C64/fesquareDisplay.log index 006b83cd9..8eb7c9e67 100644 --- a/src/Specific/X25519/C64/fesquareDisplay.log +++ b/src/Specific/X25519/C64/fesquareDisplay.log @@ -2,36 +2,36 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x7, x8, x6, x4, x2)%core, - uint64_t x9 = x2 * 0x2; - uint64_t x10 = x4 * 0x2; - uint64_t x11 = x6 * 0x2 * 0x13; - uint64_t x12 = x7 * 0x13; - uint64_t x13 = x12 * 0x2; - uint128_t x14 = (uint128_t) x2 * x2 + (uint128_t) x13 * x4 + (uint128_t) x11 * x8; - uint128_t x15 = (uint128_t) x9 * x4 + (uint128_t) x13 * x6 + (uint128_t) x8 * (x8 * 0x13); - uint128_t x16 = (uint128_t) x9 * x6 + (uint128_t) x4 * x4 + (uint128_t) x13 * x8; - uint128_t x17 = (uint128_t) x9 * x8 + (uint128_t) x10 * x6 + (uint128_t) x7 * x12; - uint128_t x18 = (uint128_t) x9 * x7 + (uint128_t) x10 * x8 + (uint128_t) x6 * x6; + uint64_t x9 = (x2 * 0x2); + uint64_t x10 = (x4 * 0x2); + uint64_t x11 = ((x6 * 0x2) * 0x13); + uint64_t x12 = (x7 * 0x13); + uint64_t x13 = (x12 * 0x2); + uint128_t x14 = ((((uint128_t)x2 * x2) + ((uint128_t)x13 * x4)) + ((uint128_t)x11 * x8)); + uint128_t x15 = ((((uint128_t)x9 * x4) + ((uint128_t)x13 * x6)) + ((uint128_t)x8 * (x8 * 0x13))); + uint128_t x16 = ((((uint128_t)x9 * x6) + ((uint128_t)x4 * x4)) + ((uint128_t)x13 * x8)); + uint128_t x17 = ((((uint128_t)x9 * x8) + ((uint128_t)x10 * x6)) + ((uint128_t)x7 * x12)); + uint128_t x18 = ((((uint128_t)x9 * x7) + ((uint128_t)x10 * x8)) + ((uint128_t)x6 * x6)); uint64_t x19 = (uint64_t) (x14 >> 0x33); - uint64_t x20 = (uint64_t) x14 & 0x7ffffffffffff; - uint128_t x21 = x19 + x15; + uint64_t x20 = ((uint64_t)x14 & 0x7ffffffffffff); + uint128_t x21 = (x19 + x15); uint64_t x22 = (uint64_t) (x21 >> 0x33); - uint64_t x23 = (uint64_t) x21 & 0x7ffffffffffff; - uint128_t x24 = x22 + x16; + uint64_t x23 = ((uint64_t)x21 & 0x7ffffffffffff); + uint128_t x24 = (x22 + x16); uint64_t x25 = (uint64_t) (x24 >> 0x33); - uint64_t x26 = (uint64_t) x24 & 0x7ffffffffffff; - uint128_t x27 = x25 + x17; + uint64_t x26 = ((uint64_t)x24 & 0x7ffffffffffff); + uint128_t x27 = (x25 + x17); uint64_t x28 = (uint64_t) (x27 >> 0x33); - uint64_t x29 = (uint64_t) x27 & 0x7ffffffffffff; - uint128_t x30 = x28 + x18; + uint64_t x29 = ((uint64_t)x27 & 0x7ffffffffffff); + uint128_t x30 = (x28 + x18); uint64_t x31 = (uint64_t) (x30 >> 0x33); - uint64_t x32 = (uint64_t) x30 & 0x7ffffffffffff; - uint64_t x33 = x20 + 0x13 * x31; - uint64_t x34 = x33 >> 0x33; - uint64_t x35 = x33 & 0x7ffffffffffff; - uint64_t x36 = x34 + x23; - uint64_t x37 = x36 >> 0x33; - uint64_t x38 = x36 & 0x7ffffffffffff; - return (Return x32, Return x29, x37 + x26, Return x38, Return x35)) + uint64_t x32 = ((uint64_t)x30 & 0x7ffffffffffff); + uint64_t x33 = (x20 + (0x13 * x31)); + uint64_t x34 = (x33 >> 0x33); + uint64_t x35 = (x33 & 0x7ffffffffffff); + uint64_t x36 = (x34 + x23); + uint64_t x37 = (x36 >> 0x33); + uint64_t x38 = (x36 & 0x7ffffffffffff); + return (Return x32, Return x29, (x37 + x26), Return x38, Return x35)) x : word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/X25519/C64/ladderstepDisplay.log b/src/Specific/X25519/C64/ladderstepDisplay.log index 56c67eeb2..ca8ba4396 100644 --- a/src/Specific/X25519/C64/ladderstepDisplay.log +++ b/src/Specific/X25519/C64/ladderstepDisplay.log @@ -2,366 +2,366 @@ let (a, b) := Interp-η (λ var : Syntax.base_type → Type, λ '(x15, x16, x14, x12, x10, (x25, x26, x24, x22, x20, (x33, x34, x32, x30, x28)), (x43, x44, x42, x40, x38, (x51, x52, x50, x48, x46)))%core, - uint64_t x53 = x25 + x33; - uint64_t x54 = x26 + x34; - uint64_t x55 = x24 + x32; - uint64_t x56 = x22 + x30; - uint64_t x57 = x20 + x28; - uint64_t x58 = 0xffffffffffffe + x25 - x33; - uint64_t x59 = 0xffffffffffffe + x26 - x34; - uint64_t x60 = 0xffffffffffffe + x24 - x32; - uint64_t x61 = 0xffffffffffffe + x22 - x30; - uint64_t x62 = 0xfffffffffffda + x20 - x28; - uint64_t x63 = x43 + x51; - uint64_t x64 = x44 + x52; - uint64_t x65 = x42 + x50; - uint64_t x66 = x40 + x48; - uint64_t x67 = x38 + x46; - uint64_t x68 = 0xffffffffffffe + x43 - x51; - uint64_t x69 = 0xffffffffffffe + x44 - x52; - uint64_t x70 = 0xffffffffffffe + x42 - x50; - uint64_t x71 = 0xffffffffffffe + x40 - x48; - uint64_t x72 = 0xfffffffffffda + x38 - x46; - uint128_t x73 = (uint128_t) x67 * x62; - uint128_t x74 = (uint128_t) x67 * x61 + (uint128_t) x66 * x62; - uint128_t x75 = (uint128_t) x67 * x60 + (uint128_t) x65 * x62 + (uint128_t) x66 * x61; - uint128_t x76 = (uint128_t) x67 * x59 + (uint128_t) x64 * x62 + (uint128_t) x66 * x60 + (uint128_t) x65 * x61; - uint128_t x77 = (uint128_t) x67 * x58 + (uint128_t) x63 * x62 + (uint128_t) x64 * x61 + (uint128_t) x66 * x59 + (uint128_t) x65 * x60; - uint64_t x78 = x63 * 0x13; - uint64_t x79 = x66 * 0x13; - uint64_t x80 = x65 * 0x13; - uint64_t x81 = x64 * 0x13; - uint128_t x82 = x73 + (uint128_t) x78 * x61 + (uint128_t) x79 * x58 + (uint128_t) x80 * x59 + (uint128_t) x81 * x60; - uint128_t x83 = x74 + (uint128_t) x78 * x60 + (uint128_t) x80 * x58 + (uint128_t) x81 * x59; - uint128_t x84 = x75 + (uint128_t) x78 * x59 + (uint128_t) x81 * x58; - uint128_t x85 = x76 + (uint128_t) x78 * x58; + uint64_t x53 = (x25 + x33); + uint64_t x54 = (x26 + x34); + uint64_t x55 = (x24 + x32); + uint64_t x56 = (x22 + x30); + uint64_t x57 = (x20 + x28); + uint64_t x58 = ((0xffffffffffffe + x25) - x33); + uint64_t x59 = ((0xffffffffffffe + x26) - x34); + uint64_t x60 = ((0xffffffffffffe + x24) - x32); + uint64_t x61 = ((0xffffffffffffe + x22) - x30); + uint64_t x62 = ((0xfffffffffffda + x20) - x28); + uint64_t x63 = (x43 + x51); + uint64_t x64 = (x44 + x52); + uint64_t x65 = (x42 + x50); + uint64_t x66 = (x40 + x48); + uint64_t x67 = (x38 + x46); + uint64_t x68 = ((0xffffffffffffe + x43) - x51); + uint64_t x69 = ((0xffffffffffffe + x44) - x52); + uint64_t x70 = ((0xffffffffffffe + x42) - x50); + uint64_t x71 = ((0xffffffffffffe + x40) - x48); + uint64_t x72 = ((0xfffffffffffda + x38) - x46); + uint128_t x73 = ((uint128_t)x67 * x62); + uint128_t x74 = (((uint128_t)x67 * x61) + ((uint128_t)x66 * x62)); + uint128_t x75 = ((((uint128_t)x67 * x60) + ((uint128_t)x65 * x62)) + ((uint128_t)x66 * x61)); + uint128_t x76 = (((((uint128_t)x67 * x59) + ((uint128_t)x64 * x62)) + ((uint128_t)x66 * x60)) + ((uint128_t)x65 * x61)); + uint128_t x77 = ((((((uint128_t)x67 * x58) + ((uint128_t)x63 * x62)) + ((uint128_t)x64 * x61)) + ((uint128_t)x66 * x59)) + ((uint128_t)x65 * x60)); + uint64_t x78 = (x63 * 0x13); + uint64_t x79 = (x66 * 0x13); + uint64_t x80 = (x65 * 0x13); + uint64_t x81 = (x64 * 0x13); + uint128_t x82 = ((((x73 + ((uint128_t)x78 * x61)) + ((uint128_t)x79 * x58)) + ((uint128_t)x80 * x59)) + ((uint128_t)x81 * x60)); + uint128_t x83 = (((x74 + ((uint128_t)x78 * x60)) + ((uint128_t)x80 * x58)) + ((uint128_t)x81 * x59)); + uint128_t x84 = ((x75 + ((uint128_t)x78 * x59)) + ((uint128_t)x81 * x58)); + uint128_t x85 = (x76 + ((uint128_t)x78 * x58)); uint64_t x86 = (uint64_t) (x82 >> 0x33); - uint64_t x87 = (uint64_t) x82 & 0x7ffffffffffff; - uint128_t x88 = x86 + x83; + uint64_t x87 = ((uint64_t)x82 & 0x7ffffffffffff); + uint128_t x88 = (x86 + x83); uint64_t x89 = (uint64_t) (x88 >> 0x33); - uint64_t x90 = (uint64_t) x88 & 0x7ffffffffffff; - uint128_t x91 = x89 + x84; + uint64_t x90 = ((uint64_t)x88 & 0x7ffffffffffff); + uint128_t x91 = (x89 + x84); uint64_t x92 = (uint64_t) (x91 >> 0x33); - uint64_t x93 = (uint64_t) x91 & 0x7ffffffffffff; - uint128_t x94 = x92 + x85; + uint64_t x93 = ((uint64_t)x91 & 0x7ffffffffffff); + uint128_t x94 = (x92 + x85); uint64_t x95 = (uint64_t) (x94 >> 0x33); - uint64_t x96 = (uint64_t) x94 & 0x7ffffffffffff; - uint128_t x97 = x95 + x77; + uint64_t x96 = ((uint64_t)x94 & 0x7ffffffffffff); + uint128_t x97 = (x95 + x77); uint64_t x98 = (uint64_t) (x97 >> 0x33); - uint64_t x99 = (uint64_t) x97 & 0x7ffffffffffff; - uint64_t x100 = x87 + 0x13 * x98; - uint64_t x101 = x100 >> 0x33; - uint64_t x102 = x100 & 0x7ffffffffffff; - uint64_t x103 = x101 + x90; - uint64_t x104 = x103 >> 0x33; - uint64_t x105 = x103 & 0x7ffffffffffff; - uint64_t x106 = x104 + x93; - uint128_t x107 = (uint128_t) x57 * x72; - uint128_t x108 = (uint128_t) x57 * x71 + (uint128_t) x56 * x72; - uint128_t x109 = (uint128_t) x57 * x70 + (uint128_t) x55 * x72 + (uint128_t) x56 * x71; - uint128_t x110 = (uint128_t) x57 * x69 + (uint128_t) x54 * x72 + (uint128_t) x56 * x70 + (uint128_t) x55 * x71; - uint128_t x111 = (uint128_t) x57 * x68 + (uint128_t) x53 * x72 + (uint128_t) x54 * x71 + (uint128_t) x56 * x69 + (uint128_t) x55 * x70; - uint64_t x112 = x53 * 0x13; - uint64_t x113 = x56 * 0x13; - uint64_t x114 = x55 * 0x13; - uint64_t x115 = x54 * 0x13; - uint128_t x116 = x107 + (uint128_t) x112 * x71 + (uint128_t) x113 * x68 + (uint128_t) x114 * x69 + (uint128_t) x115 * x70; - uint128_t x117 = x108 + (uint128_t) x112 * x70 + (uint128_t) x114 * x68 + (uint128_t) x115 * x69; - uint128_t x118 = x109 + (uint128_t) x112 * x69 + (uint128_t) x115 * x68; - uint128_t x119 = x110 + (uint128_t) x112 * x68; + uint64_t x99 = ((uint64_t)x97 & 0x7ffffffffffff); + uint64_t x100 = (x87 + (0x13 * x98)); + uint64_t x101 = (x100 >> 0x33); + uint64_t x102 = (x100 & 0x7ffffffffffff); + uint64_t x103 = (x101 + x90); + uint64_t x104 = (x103 >> 0x33); + uint64_t x105 = (x103 & 0x7ffffffffffff); + uint64_t x106 = (x104 + x93); + uint128_t x107 = ((uint128_t)x57 * x72); + uint128_t x108 = (((uint128_t)x57 * x71) + ((uint128_t)x56 * x72)); + uint128_t x109 = ((((uint128_t)x57 * x70) + ((uint128_t)x55 * x72)) + ((uint128_t)x56 * x71)); + uint128_t x110 = (((((uint128_t)x57 * x69) + ((uint128_t)x54 * x72)) + ((uint128_t)x56 * x70)) + ((uint128_t)x55 * x71)); + uint128_t x111 = ((((((uint128_t)x57 * x68) + ((uint128_t)x53 * x72)) + ((uint128_t)x54 * x71)) + ((uint128_t)x56 * x69)) + ((uint128_t)x55 * x70)); + uint64_t x112 = (x53 * 0x13); + uint64_t x113 = (x56 * 0x13); + uint64_t x114 = (x55 * 0x13); + uint64_t x115 = (x54 * 0x13); + uint128_t x116 = ((((x107 + ((uint128_t)x112 * x71)) + ((uint128_t)x113 * x68)) + ((uint128_t)x114 * x69)) + ((uint128_t)x115 * x70)); + uint128_t x117 = (((x108 + ((uint128_t)x112 * x70)) + ((uint128_t)x114 * x68)) + ((uint128_t)x115 * x69)); + uint128_t x118 = ((x109 + ((uint128_t)x112 * x69)) + ((uint128_t)x115 * x68)); + uint128_t x119 = (x110 + ((uint128_t)x112 * x68)); uint64_t x120 = (uint64_t) (x116 >> 0x33); - uint64_t x121 = (uint64_t) x116 & 0x7ffffffffffff; - uint128_t x122 = x120 + x117; + uint64_t x121 = ((uint64_t)x116 & 0x7ffffffffffff); + uint128_t x122 = (x120 + x117); uint64_t x123 = (uint64_t) (x122 >> 0x33); - uint64_t x124 = (uint64_t) x122 & 0x7ffffffffffff; - uint128_t x125 = x123 + x118; + uint64_t x124 = ((uint64_t)x122 & 0x7ffffffffffff); + uint128_t x125 = (x123 + x118); uint64_t x126 = (uint64_t) (x125 >> 0x33); - uint64_t x127 = (uint64_t) x125 & 0x7ffffffffffff; - uint128_t x128 = x126 + x119; + uint64_t x127 = ((uint64_t)x125 & 0x7ffffffffffff); + uint128_t x128 = (x126 + x119); uint64_t x129 = (uint64_t) (x128 >> 0x33); - uint64_t x130 = (uint64_t) x128 & 0x7ffffffffffff; - uint128_t x131 = x129 + x111; + uint64_t x130 = ((uint64_t)x128 & 0x7ffffffffffff); + uint128_t x131 = (x129 + x111); uint64_t x132 = (uint64_t) (x131 >> 0x33); - uint64_t x133 = (uint64_t) x131 & 0x7ffffffffffff; - uint64_t x134 = x121 + 0x13 * x132; - uint64_t x135 = x134 >> 0x33; - uint64_t x136 = x134 & 0x7ffffffffffff; - uint64_t x137 = x135 + x124; - uint64_t x138 = x137 >> 0x33; - uint64_t x139 = x137 & 0x7ffffffffffff; - uint64_t x140 = x138 + x127; - uint64_t x141 = x99 + x133; - uint64_t x142 = x96 + x130; - uint64_t x143 = x106 + x140; - uint64_t x144 = x105 + x139; - uint64_t x145 = x102 + x136; - uint64_t x146 = 0xffffffffffffe + x99 - x133; - uint64_t x147 = 0xffffffffffffe + x96 - x130; - uint64_t x148 = 0xffffffffffffe + x106 - x140; - uint64_t x149 = 0xffffffffffffe + x105 - x139; - uint64_t x150 = 0xfffffffffffda + x102 - x136; - uint64_t x151 = x145 * 0x2; - uint64_t x152 = x144 * 0x2; - uint64_t x153 = x143 * 0x2 * 0x13; - uint64_t x154 = x141 * 0x13; - uint64_t x155 = x154 * 0x2; - uint128_t x156 = (uint128_t) x145 * x145 + (uint128_t) x155 * x144 + (uint128_t) x153 * x142; - uint128_t x157 = (uint128_t) x151 * x144 + (uint128_t) x155 * x143 + (uint128_t) x142 * (x142 * 0x13); - uint128_t x158 = (uint128_t) x151 * x143 + (uint128_t) x144 * x144 + (uint128_t) x155 * x142; - uint128_t x159 = (uint128_t) x151 * x142 + (uint128_t) x152 * x143 + (uint128_t) x141 * x154; - uint128_t x160 = (uint128_t) x151 * x141 + (uint128_t) x152 * x142 + (uint128_t) x143 * x143; + uint64_t x133 = ((uint64_t)x131 & 0x7ffffffffffff); + uint64_t x134 = (x121 + (0x13 * x132)); + uint64_t x135 = (x134 >> 0x33); + uint64_t x136 = (x134 & 0x7ffffffffffff); + uint64_t x137 = (x135 + x124); + uint64_t x138 = (x137 >> 0x33); + uint64_t x139 = (x137 & 0x7ffffffffffff); + uint64_t x140 = (x138 + x127); + uint64_t x141 = (x99 + x133); + uint64_t x142 = (x96 + x130); + uint64_t x143 = (x106 + x140); + uint64_t x144 = (x105 + x139); + uint64_t x145 = (x102 + x136); + uint64_t x146 = ((0xffffffffffffe + x99) - x133); + uint64_t x147 = ((0xffffffffffffe + x96) - x130); + uint64_t x148 = ((0xffffffffffffe + x106) - x140); + uint64_t x149 = ((0xffffffffffffe + x105) - x139); + uint64_t x150 = ((0xfffffffffffda + x102) - x136); + uint64_t x151 = (x145 * 0x2); + uint64_t x152 = (x144 * 0x2); + uint64_t x153 = ((x143 * 0x2) * 0x13); + uint64_t x154 = (x141 * 0x13); + uint64_t x155 = (x154 * 0x2); + uint128_t x156 = ((((uint128_t)x145 * x145) + ((uint128_t)x155 * x144)) + ((uint128_t)x153 * x142)); + uint128_t x157 = ((((uint128_t)x151 * x144) + ((uint128_t)x155 * x143)) + ((uint128_t)x142 * (x142 * 0x13))); + uint128_t x158 = ((((uint128_t)x151 * x143) + ((uint128_t)x144 * x144)) + ((uint128_t)x155 * x142)); + uint128_t x159 = ((((uint128_t)x151 * x142) + ((uint128_t)x152 * x143)) + ((uint128_t)x141 * x154)); + uint128_t x160 = ((((uint128_t)x151 * x141) + ((uint128_t)x152 * x142)) + ((uint128_t)x143 * x143)); uint64_t x161 = (uint64_t) (x156 >> 0x33); - uint64_t x162 = (uint64_t) x156 & 0x7ffffffffffff; - uint128_t x163 = x161 + x157; + uint64_t x162 = ((uint64_t)x156 & 0x7ffffffffffff); + uint128_t x163 = (x161 + x157); uint64_t x164 = (uint64_t) (x163 >> 0x33); - uint64_t x165 = (uint64_t) x163 & 0x7ffffffffffff; - uint128_t x166 = x164 + x158; + uint64_t x165 = ((uint64_t)x163 & 0x7ffffffffffff); + uint128_t x166 = (x164 + x158); uint64_t x167 = (uint64_t) (x166 >> 0x33); - uint64_t x168 = (uint64_t) x166 & 0x7ffffffffffff; - uint128_t x169 = x167 + x159; + uint64_t x168 = ((uint64_t)x166 & 0x7ffffffffffff); + uint128_t x169 = (x167 + x159); uint64_t x170 = (uint64_t) (x169 >> 0x33); - uint64_t x171 = (uint64_t) x169 & 0x7ffffffffffff; - uint128_t x172 = x170 + x160; + uint64_t x171 = ((uint64_t)x169 & 0x7ffffffffffff); + uint128_t x172 = (x170 + x160); uint64_t x173 = (uint64_t) (x172 >> 0x33); - uint64_t x174 = (uint64_t) x172 & 0x7ffffffffffff; - uint64_t x175 = x162 + 0x13 * x173; - uint64_t x176 = x175 >> 0x33; - uint64_t x177 = x175 & 0x7ffffffffffff; - uint64_t x178 = x176 + x165; - uint64_t x179 = x178 >> 0x33; - uint64_t x180 = x178 & 0x7ffffffffffff; - uint64_t x181 = x179 + x168; - uint64_t x182 = x150 * 0x2; - uint64_t x183 = x149 * 0x2; - uint64_t x184 = x148 * 0x2 * 0x13; - uint64_t x185 = x146 * 0x13; - uint64_t x186 = x185 * 0x2; - uint128_t x187 = (uint128_t) x150 * x150 + (uint128_t) x186 * x149 + (uint128_t) x184 * x147; - uint128_t x188 = (uint128_t) x182 * x149 + (uint128_t) x186 * x148 + (uint128_t) x147 * (x147 * 0x13); - uint128_t x189 = (uint128_t) x182 * x148 + (uint128_t) x149 * x149 + (uint128_t) x186 * x147; - uint128_t x190 = (uint128_t) x182 * x147 + (uint128_t) x183 * x148 + (uint128_t) x146 * x185; - uint128_t x191 = (uint128_t) x182 * x146 + (uint128_t) x183 * x147 + (uint128_t) x148 * x148; + uint64_t x174 = ((uint64_t)x172 & 0x7ffffffffffff); + uint64_t x175 = (x162 + (0x13 * x173)); + uint64_t x176 = (x175 >> 0x33); + uint64_t x177 = (x175 & 0x7ffffffffffff); + uint64_t x178 = (x176 + x165); + uint64_t x179 = (x178 >> 0x33); + uint64_t x180 = (x178 & 0x7ffffffffffff); + uint64_t x181 = (x179 + x168); + uint64_t x182 = (x150 * 0x2); + uint64_t x183 = (x149 * 0x2); + uint64_t x184 = ((x148 * 0x2) * 0x13); + uint64_t x185 = (x146 * 0x13); + uint64_t x186 = (x185 * 0x2); + uint128_t x187 = ((((uint128_t)x150 * x150) + ((uint128_t)x186 * x149)) + ((uint128_t)x184 * x147)); + uint128_t x188 = ((((uint128_t)x182 * x149) + ((uint128_t)x186 * x148)) + ((uint128_t)x147 * (x147 * 0x13))); + uint128_t x189 = ((((uint128_t)x182 * x148) + ((uint128_t)x149 * x149)) + ((uint128_t)x186 * x147)); + uint128_t x190 = ((((uint128_t)x182 * x147) + ((uint128_t)x183 * x148)) + ((uint128_t)x146 * x185)); + uint128_t x191 = ((((uint128_t)x182 * x146) + ((uint128_t)x183 * x147)) + ((uint128_t)x148 * x148)); uint64_t x192 = (uint64_t) (x187 >> 0x33); - uint64_t x193 = (uint64_t) x187 & 0x7ffffffffffff; - uint128_t x194 = x192 + x188; + uint64_t x193 = ((uint64_t)x187 & 0x7ffffffffffff); + uint128_t x194 = (x192 + x188); uint64_t x195 = (uint64_t) (x194 >> 0x33); - uint64_t x196 = (uint64_t) x194 & 0x7ffffffffffff; - uint128_t x197 = x195 + x189; + uint64_t x196 = ((uint64_t)x194 & 0x7ffffffffffff); + uint128_t x197 = (x195 + x189); uint64_t x198 = (uint64_t) (x197 >> 0x33); - uint64_t x199 = (uint64_t) x197 & 0x7ffffffffffff; - uint128_t x200 = x198 + x190; + uint64_t x199 = ((uint64_t)x197 & 0x7ffffffffffff); + uint128_t x200 = (x198 + x190); uint64_t x201 = (uint64_t) (x200 >> 0x33); - uint64_t x202 = (uint64_t) x200 & 0x7ffffffffffff; - uint128_t x203 = x201 + x191; + uint64_t x202 = ((uint64_t)x200 & 0x7ffffffffffff); + uint128_t x203 = (x201 + x191); uint64_t x204 = (uint64_t) (x203 >> 0x33); - uint64_t x205 = (uint64_t) x203 & 0x7ffffffffffff; - uint64_t x206 = x193 + 0x13 * x204; - uint64_t x207 = x206 >> 0x33; - uint64_t x208 = x206 & 0x7ffffffffffff; - uint64_t x209 = x207 + x196; - uint64_t x210 = x209 >> 0x33; - uint64_t x211 = x209 & 0x7ffffffffffff; - uint64_t x212 = x210 + x199; - uint128_t x213 = (uint128_t) x208 * x10; - uint128_t x214 = (uint128_t) x208 * x12 + (uint128_t) x211 * x10; - uint128_t x215 = (uint128_t) x208 * x14 + (uint128_t) x212 * x10 + (uint128_t) x211 * x12; - uint128_t x216 = (uint128_t) x208 * x16 + (uint128_t) x202 * x10 + (uint128_t) x211 * x14 + (uint128_t) x212 * x12; - uint128_t x217 = (uint128_t) x208 * x15 + (uint128_t) x205 * x10 + (uint128_t) x202 * x12 + (uint128_t) x211 * x16 + (uint128_t) x212 * x14; - uint64_t x218 = x205 * 0x13; - uint64_t x219 = x211 * 0x13; - uint64_t x220 = x212 * 0x13; - uint64_t x221 = x202 * 0x13; - uint128_t x222 = x213 + (uint128_t) x218 * x12 + (uint128_t) x219 * x15 + (uint128_t) x220 * x16 + (uint128_t) x221 * x14; - uint128_t x223 = x214 + (uint128_t) x218 * x14 + (uint128_t) x220 * x15 + (uint128_t) x221 * x16; - uint128_t x224 = x215 + (uint128_t) x218 * x16 + (uint128_t) x221 * x15; - uint128_t x225 = x216 + (uint128_t) x218 * x15; + uint64_t x205 = ((uint64_t)x203 & 0x7ffffffffffff); + uint64_t x206 = (x193 + (0x13 * x204)); + uint64_t x207 = (x206 >> 0x33); + uint64_t x208 = (x206 & 0x7ffffffffffff); + uint64_t x209 = (x207 + x196); + uint64_t x210 = (x209 >> 0x33); + uint64_t x211 = (x209 & 0x7ffffffffffff); + uint64_t x212 = (x210 + x199); + uint128_t x213 = ((uint128_t)x208 * x10); + uint128_t x214 = (((uint128_t)x208 * x12) + ((uint128_t)x211 * x10)); + uint128_t x215 = ((((uint128_t)x208 * x14) + ((uint128_t)x212 * x10)) + ((uint128_t)x211 * x12)); + uint128_t x216 = (((((uint128_t)x208 * x16) + ((uint128_t)x202 * x10)) + ((uint128_t)x211 * x14)) + ((uint128_t)x212 * x12)); + uint128_t x217 = ((((((uint128_t)x208 * x15) + ((uint128_t)x205 * x10)) + ((uint128_t)x202 * x12)) + ((uint128_t)x211 * x16)) + ((uint128_t)x212 * x14)); + uint64_t x218 = (x205 * 0x13); + uint64_t x219 = (x211 * 0x13); + uint64_t x220 = (x212 * 0x13); + uint64_t x221 = (x202 * 0x13); + uint128_t x222 = ((((x213 + ((uint128_t)x218 * x12)) + ((uint128_t)x219 * x15)) + ((uint128_t)x220 * x16)) + ((uint128_t)x221 * x14)); + uint128_t x223 = (((x214 + ((uint128_t)x218 * x14)) + ((uint128_t)x220 * x15)) + ((uint128_t)x221 * x16)); + uint128_t x224 = ((x215 + ((uint128_t)x218 * x16)) + ((uint128_t)x221 * x15)); + uint128_t x225 = (x216 + ((uint128_t)x218 * x15)); uint64_t x226 = (uint64_t) (x222 >> 0x33); - uint64_t x227 = (uint64_t) x222 & 0x7ffffffffffff; - uint128_t x228 = x226 + x223; + uint64_t x227 = ((uint64_t)x222 & 0x7ffffffffffff); + uint128_t x228 = (x226 + x223); uint64_t x229 = (uint64_t) (x228 >> 0x33); - uint64_t x230 = (uint64_t) x228 & 0x7ffffffffffff; - uint128_t x231 = x229 + x224; + uint64_t x230 = ((uint64_t)x228 & 0x7ffffffffffff); + uint128_t x231 = (x229 + x224); uint64_t x232 = (uint64_t) (x231 >> 0x33); - uint64_t x233 = (uint64_t) x231 & 0x7ffffffffffff; - uint128_t x234 = x232 + x225; + uint64_t x233 = ((uint64_t)x231 & 0x7ffffffffffff); + uint128_t x234 = (x232 + x225); uint64_t x235 = (uint64_t) (x234 >> 0x33); - uint64_t x236 = (uint64_t) x234 & 0x7ffffffffffff; - uint128_t x237 = x235 + x217; + uint64_t x236 = ((uint64_t)x234 & 0x7ffffffffffff); + uint128_t x237 = (x235 + x217); uint64_t x238 = (uint64_t) (x237 >> 0x33); - uint64_t x239 = (uint64_t) x237 & 0x7ffffffffffff; - uint64_t x240 = x227 + 0x13 * x238; - uint64_t x241 = x240 >> 0x33; - uint64_t x242 = x240 & 0x7ffffffffffff; - uint64_t x243 = x241 + x230; - uint64_t x244 = x243 >> 0x33; - uint64_t x245 = x243 & 0x7ffffffffffff; - uint64_t x246 = x244 + x233; - uint64_t x247 = x57 * 0x2; - uint64_t x248 = x56 * 0x2; - uint64_t x249 = x55 * 0x2 * 0x13; - uint64_t x250 = x53 * 0x13; - uint64_t x251 = x250 * 0x2; - uint128_t x252 = (uint128_t) x57 * x57 + (uint128_t) x251 * x56 + (uint128_t) x249 * x54; - uint128_t x253 = (uint128_t) x247 * x56 + (uint128_t) x251 * x55 + (uint128_t) x54 * (x54 * 0x13); - uint128_t x254 = (uint128_t) x247 * x55 + (uint128_t) x56 * x56 + (uint128_t) x251 * x54; - uint128_t x255 = (uint128_t) x247 * x54 + (uint128_t) x248 * x55 + (uint128_t) x53 * x250; - uint128_t x256 = (uint128_t) x247 * x53 + (uint128_t) x248 * x54 + (uint128_t) x55 * x55; + uint64_t x239 = ((uint64_t)x237 & 0x7ffffffffffff); + uint64_t x240 = (x227 + (0x13 * x238)); + uint64_t x241 = (x240 >> 0x33); + uint64_t x242 = (x240 & 0x7ffffffffffff); + uint64_t x243 = (x241 + x230); + uint64_t x244 = (x243 >> 0x33); + uint64_t x245 = (x243 & 0x7ffffffffffff); + uint64_t x246 = (x244 + x233); + uint64_t x247 = (x57 * 0x2); + uint64_t x248 = (x56 * 0x2); + uint64_t x249 = ((x55 * 0x2) * 0x13); + uint64_t x250 = (x53 * 0x13); + uint64_t x251 = (x250 * 0x2); + uint128_t x252 = ((((uint128_t)x57 * x57) + ((uint128_t)x251 * x56)) + ((uint128_t)x249 * x54)); + uint128_t x253 = ((((uint128_t)x247 * x56) + ((uint128_t)x251 * x55)) + ((uint128_t)x54 * (x54 * 0x13))); + uint128_t x254 = ((((uint128_t)x247 * x55) + ((uint128_t)x56 * x56)) + ((uint128_t)x251 * x54)); + uint128_t x255 = ((((uint128_t)x247 * x54) + ((uint128_t)x248 * x55)) + ((uint128_t)x53 * x250)); + uint128_t x256 = ((((uint128_t)x247 * x53) + ((uint128_t)x248 * x54)) + ((uint128_t)x55 * x55)); uint64_t x257 = (uint64_t) (x252 >> 0x33); - uint64_t x258 = (uint64_t) x252 & 0x7ffffffffffff; - uint128_t x259 = x257 + x253; + uint64_t x258 = ((uint64_t)x252 & 0x7ffffffffffff); + uint128_t x259 = (x257 + x253); uint64_t x260 = (uint64_t) (x259 >> 0x33); - uint64_t x261 = (uint64_t) x259 & 0x7ffffffffffff; - uint128_t x262 = x260 + x254; + uint64_t x261 = ((uint64_t)x259 & 0x7ffffffffffff); + uint128_t x262 = (x260 + x254); uint64_t x263 = (uint64_t) (x262 >> 0x33); - uint64_t x264 = (uint64_t) x262 & 0x7ffffffffffff; - uint128_t x265 = x263 + x255; + uint64_t x264 = ((uint64_t)x262 & 0x7ffffffffffff); + uint128_t x265 = (x263 + x255); uint64_t x266 = (uint64_t) (x265 >> 0x33); - uint64_t x267 = (uint64_t) x265 & 0x7ffffffffffff; - uint128_t x268 = x266 + x256; + uint64_t x267 = ((uint64_t)x265 & 0x7ffffffffffff); + uint128_t x268 = (x266 + x256); uint64_t x269 = (uint64_t) (x268 >> 0x33); - uint64_t x270 = (uint64_t) x268 & 0x7ffffffffffff; - uint64_t x271 = x258 + 0x13 * x269; - uint64_t x272 = x271 >> 0x33; - uint64_t x273 = x271 & 0x7ffffffffffff; - uint64_t x274 = x272 + x261; - uint64_t x275 = x274 >> 0x33; - uint64_t x276 = x274 & 0x7ffffffffffff; - uint64_t x277 = x275 + x264; - uint64_t x278 = x62 * 0x2; - uint64_t x279 = x61 * 0x2; - uint64_t x280 = x60 * 0x2 * 0x13; - uint64_t x281 = x58 * 0x13; - uint64_t x282 = x281 * 0x2; - uint128_t x283 = (uint128_t) x62 * x62 + (uint128_t) x282 * x61 + (uint128_t) x280 * x59; - uint128_t x284 = (uint128_t) x278 * x61 + (uint128_t) x282 * x60 + (uint128_t) x59 * (x59 * 0x13); - uint128_t x285 = (uint128_t) x278 * x60 + (uint128_t) x61 * x61 + (uint128_t) x282 * x59; - uint128_t x286 = (uint128_t) x278 * x59 + (uint128_t) x279 * x60 + (uint128_t) x58 * x281; - uint128_t x287 = (uint128_t) x278 * x58 + (uint128_t) x279 * x59 + (uint128_t) x60 * x60; + uint64_t x270 = ((uint64_t)x268 & 0x7ffffffffffff); + uint64_t x271 = (x258 + (0x13 * x269)); + uint64_t x272 = (x271 >> 0x33); + uint64_t x273 = (x271 & 0x7ffffffffffff); + uint64_t x274 = (x272 + x261); + uint64_t x275 = (x274 >> 0x33); + uint64_t x276 = (x274 & 0x7ffffffffffff); + uint64_t x277 = (x275 + x264); + uint64_t x278 = (x62 * 0x2); + uint64_t x279 = (x61 * 0x2); + uint64_t x280 = ((x60 * 0x2) * 0x13); + uint64_t x281 = (x58 * 0x13); + uint64_t x282 = (x281 * 0x2); + uint128_t x283 = ((((uint128_t)x62 * x62) + ((uint128_t)x282 * x61)) + ((uint128_t)x280 * x59)); + uint128_t x284 = ((((uint128_t)x278 * x61) + ((uint128_t)x282 * x60)) + ((uint128_t)x59 * (x59 * 0x13))); + uint128_t x285 = ((((uint128_t)x278 * x60) + ((uint128_t)x61 * x61)) + ((uint128_t)x282 * x59)); + uint128_t x286 = ((((uint128_t)x278 * x59) + ((uint128_t)x279 * x60)) + ((uint128_t)x58 * x281)); + uint128_t x287 = ((((uint128_t)x278 * x58) + ((uint128_t)x279 * x59)) + ((uint128_t)x60 * x60)); uint64_t x288 = (uint64_t) (x283 >> 0x33); - uint64_t x289 = (uint64_t) x283 & 0x7ffffffffffff; - uint128_t x290 = x288 + x284; + uint64_t x289 = ((uint64_t)x283 & 0x7ffffffffffff); + uint128_t x290 = (x288 + x284); uint64_t x291 = (uint64_t) (x290 >> 0x33); - uint64_t x292 = (uint64_t) x290 & 0x7ffffffffffff; - uint128_t x293 = x291 + x285; + uint64_t x292 = ((uint64_t)x290 & 0x7ffffffffffff); + uint128_t x293 = (x291 + x285); uint64_t x294 = (uint64_t) (x293 >> 0x33); - uint64_t x295 = (uint64_t) x293 & 0x7ffffffffffff; - uint128_t x296 = x294 + x286; + uint64_t x295 = ((uint64_t)x293 & 0x7ffffffffffff); + uint128_t x296 = (x294 + x286); uint64_t x297 = (uint64_t) (x296 >> 0x33); - uint64_t x298 = (uint64_t) x296 & 0x7ffffffffffff; - uint128_t x299 = x297 + x287; + uint64_t x298 = ((uint64_t)x296 & 0x7ffffffffffff); + uint128_t x299 = (x297 + x287); uint64_t x300 = (uint64_t) (x299 >> 0x33); - uint64_t x301 = (uint64_t) x299 & 0x7ffffffffffff; - uint64_t x302 = x289 + 0x13 * x300; - uint64_t x303 = x302 >> 0x33; - uint64_t x304 = x302 & 0x7ffffffffffff; - uint64_t x305 = x303 + x292; - uint64_t x306 = x305 >> 0x33; - uint64_t x307 = x305 & 0x7ffffffffffff; - uint64_t x308 = x306 + x295; - uint128_t x309 = (uint128_t) x273 * x304; - uint128_t x310 = (uint128_t) x273 * x307 + (uint128_t) x276 * x304; - uint128_t x311 = (uint128_t) x273 * x308 + (uint128_t) x277 * x304 + (uint128_t) x276 * x307; - uint128_t x312 = (uint128_t) x273 * x298 + (uint128_t) x267 * x304 + (uint128_t) x276 * x308 + (uint128_t) x277 * x307; - uint128_t x313 = (uint128_t) x273 * x301 + (uint128_t) x270 * x304 + (uint128_t) x267 * x307 + (uint128_t) x276 * x298 + (uint128_t) x277 * x308; - uint64_t x314 = x270 * 0x13; - uint64_t x315 = x276 * 0x13; - uint64_t x316 = x277 * 0x13; - uint64_t x317 = x267 * 0x13; - uint128_t x318 = x309 + (uint128_t) x314 * x307 + (uint128_t) x315 * x301 + (uint128_t) x316 * x298 + (uint128_t) x317 * x308; - uint128_t x319 = x310 + (uint128_t) x314 * x308 + (uint128_t) x316 * x301 + (uint128_t) x317 * x298; - uint128_t x320 = x311 + (uint128_t) x314 * x298 + (uint128_t) x317 * x301; - uint128_t x321 = x312 + (uint128_t) x314 * x301; + uint64_t x301 = ((uint64_t)x299 & 0x7ffffffffffff); + uint64_t x302 = (x289 + (0x13 * x300)); + uint64_t x303 = (x302 >> 0x33); + uint64_t x304 = (x302 & 0x7ffffffffffff); + uint64_t x305 = (x303 + x292); + uint64_t x306 = (x305 >> 0x33); + uint64_t x307 = (x305 & 0x7ffffffffffff); + uint64_t x308 = (x306 + x295); + uint128_t x309 = ((uint128_t)x273 * x304); + uint128_t x310 = (((uint128_t)x273 * x307) + ((uint128_t)x276 * x304)); + uint128_t x311 = ((((uint128_t)x273 * x308) + ((uint128_t)x277 * x304)) + ((uint128_t)x276 * x307)); + uint128_t x312 = (((((uint128_t)x273 * x298) + ((uint128_t)x267 * x304)) + ((uint128_t)x276 * x308)) + ((uint128_t)x277 * x307)); + uint128_t x313 = ((((((uint128_t)x273 * x301) + ((uint128_t)x270 * x304)) + ((uint128_t)x267 * x307)) + ((uint128_t)x276 * x298)) + ((uint128_t)x277 * x308)); + uint64_t x314 = (x270 * 0x13); + uint64_t x315 = (x276 * 0x13); + uint64_t x316 = (x277 * 0x13); + uint64_t x317 = (x267 * 0x13); + uint128_t x318 = ((((x309 + ((uint128_t)x314 * x307)) + ((uint128_t)x315 * x301)) + ((uint128_t)x316 * x298)) + ((uint128_t)x317 * x308)); + uint128_t x319 = (((x310 + ((uint128_t)x314 * x308)) + ((uint128_t)x316 * x301)) + ((uint128_t)x317 * x298)); + uint128_t x320 = ((x311 + ((uint128_t)x314 * x298)) + ((uint128_t)x317 * x301)); + uint128_t x321 = (x312 + ((uint128_t)x314 * x301)); uint64_t x322 = (uint64_t) (x318 >> 0x33); - uint64_t x323 = (uint64_t) x318 & 0x7ffffffffffff; - uint128_t x324 = x322 + x319; + uint64_t x323 = ((uint64_t)x318 & 0x7ffffffffffff); + uint128_t x324 = (x322 + x319); uint64_t x325 = (uint64_t) (x324 >> 0x33); - uint64_t x326 = (uint64_t) x324 & 0x7ffffffffffff; - uint128_t x327 = x325 + x320; + uint64_t x326 = ((uint64_t)x324 & 0x7ffffffffffff); + uint128_t x327 = (x325 + x320); uint64_t x328 = (uint64_t) (x327 >> 0x33); - uint64_t x329 = (uint64_t) x327 & 0x7ffffffffffff; - uint128_t x330 = x328 + x321; + uint64_t x329 = ((uint64_t)x327 & 0x7ffffffffffff); + uint128_t x330 = (x328 + x321); uint64_t x331 = (uint64_t) (x330 >> 0x33); - uint64_t x332 = (uint64_t) x330 & 0x7ffffffffffff; - uint128_t x333 = x331 + x313; + uint64_t x332 = ((uint64_t)x330 & 0x7ffffffffffff); + uint128_t x333 = (x331 + x313); uint64_t x334 = (uint64_t) (x333 >> 0x33); - uint64_t x335 = (uint64_t) x333 & 0x7ffffffffffff; - uint64_t x336 = x323 + 0x13 * x334; - uint64_t x337 = x336 >> 0x33; - uint64_t x338 = x336 & 0x7ffffffffffff; - uint64_t x339 = x337 + x326; - uint64_t x340 = x339 >> 0x33; - uint64_t x341 = x339 & 0x7ffffffffffff; - uint64_t x342 = x340 + x329; - uint64_t x343 = 0xffffffffffffe + x270 - x301; - uint64_t x344 = 0xffffffffffffe + x267 - x298; - uint64_t x345 = 0xffffffffffffe + x277 - x308; - uint64_t x346 = 0xffffffffffffe + x276 - x307; - uint64_t x347 = 0xfffffffffffda + x273 - x304; - uint128_t x348 = (uint128_t) x347 * 0x1db41; - uint128_t x349 = (uint128_t) x346 * 0x1db41; - uint128_t x350 = (uint128_t) x345 * 0x1db41; - uint128_t x351 = (uint128_t) x344 * 0x1db41; - uint128_t x352 = (uint128_t) x343 * 0x1db41; + uint64_t x335 = ((uint64_t)x333 & 0x7ffffffffffff); + uint64_t x336 = (x323 + (0x13 * x334)); + uint64_t x337 = (x336 >> 0x33); + uint64_t x338 = (x336 & 0x7ffffffffffff); + uint64_t x339 = (x337 + x326); + uint64_t x340 = (x339 >> 0x33); + uint64_t x341 = (x339 & 0x7ffffffffffff); + uint64_t x342 = (x340 + x329); + uint64_t x343 = ((0xffffffffffffe + x270) - x301); + uint64_t x344 = ((0xffffffffffffe + x267) - x298); + uint64_t x345 = ((0xffffffffffffe + x277) - x308); + uint64_t x346 = ((0xffffffffffffe + x276) - x307); + uint64_t x347 = ((0xfffffffffffda + x273) - x304); + uint128_t x348 = ((uint128_t)x347 * 0x1db41); + uint128_t x349 = ((uint128_t)x346 * 0x1db41); + uint128_t x350 = ((uint128_t)x345 * 0x1db41); + uint128_t x351 = ((uint128_t)x344 * 0x1db41); + uint128_t x352 = ((uint128_t)x343 * 0x1db41); uint64_t x353 = (uint64_t) (x348 >> 0x33); - uint64_t x354 = (uint64_t) x348 & 0x7ffffffffffff; - uint128_t x355 = x353 + x349; + uint64_t x354 = ((uint64_t)x348 & 0x7ffffffffffff); + uint128_t x355 = (x353 + x349); uint64_t x356 = (uint64_t) (x355 >> 0x33); - uint64_t x357 = (uint64_t) x355 & 0x7ffffffffffff; - uint128_t x358 = x356 + x350; + uint64_t x357 = ((uint64_t)x355 & 0x7ffffffffffff); + uint128_t x358 = (x356 + x350); uint64_t x359 = (uint64_t) (x358 >> 0x33); - uint64_t x360 = (uint64_t) x358 & 0x7ffffffffffff; - uint128_t x361 = x359 + x351; + uint64_t x360 = ((uint64_t)x358 & 0x7ffffffffffff); + uint128_t x361 = (x359 + x351); uint64_t x362 = (uint64_t) (x361 >> 0x33); - uint64_t x363 = (uint64_t) x361 & 0x7ffffffffffff; - uint128_t x364 = x362 + x352; + uint64_t x363 = ((uint64_t)x361 & 0x7ffffffffffff); + uint128_t x364 = (x362 + x352); uint64_t x365 = (uint64_t) (x364 >> 0x33); - uint64_t x366 = (uint64_t) x364 & 0x7ffffffffffff; - uint64_t x367 = x354 + 0x13 * x365; - uint64_t x368 = x367 >> 0x33; - uint64_t x369 = x367 & 0x7ffffffffffff; - uint64_t x370 = x368 + x357; - uint64_t x371 = x370 >> 0x33; - uint64_t x372 = x370 & 0x7ffffffffffff; - uint64_t x373 = x371 + x360; - uint64_t x374 = x366 + x270; - uint64_t x375 = x363 + x267; - uint64_t x376 = x373 + x277; - uint64_t x377 = x372 + x276; - uint64_t x378 = x369 + x273; - uint128_t x379 = (uint128_t) x347 * x378; - uint128_t x380 = (uint128_t) x347 * x377 + (uint128_t) x346 * x378; - uint128_t x381 = (uint128_t) x347 * x376 + (uint128_t) x345 * x378 + (uint128_t) x346 * x377; - uint128_t x382 = (uint128_t) x347 * x375 + (uint128_t) x344 * x378 + (uint128_t) x346 * x376 + (uint128_t) x345 * x377; - uint128_t x383 = (uint128_t) x347 * x374 + (uint128_t) x343 * x378 + (uint128_t) x344 * x377 + (uint128_t) x346 * x375 + (uint128_t) x345 * x376; - uint64_t x384 = x343 * 0x13; - uint64_t x385 = x346 * 0x13; - uint64_t x386 = x345 * 0x13; - uint64_t x387 = x344 * 0x13; - uint128_t x388 = x379 + (uint128_t) x384 * x377 + (uint128_t) x385 * x374 + (uint128_t) x386 * x375 + (uint128_t) x387 * x376; - uint128_t x389 = x380 + (uint128_t) x384 * x376 + (uint128_t) x386 * x374 + (uint128_t) x387 * x375; - uint128_t x390 = x381 + (uint128_t) x384 * x375 + (uint128_t) x387 * x374; - uint128_t x391 = x382 + (uint128_t) x384 * x374; + uint64_t x366 = ((uint64_t)x364 & 0x7ffffffffffff); + uint64_t x367 = (x354 + (0x13 * x365)); + uint64_t x368 = (x367 >> 0x33); + uint64_t x369 = (x367 & 0x7ffffffffffff); + uint64_t x370 = (x368 + x357); + uint64_t x371 = (x370 >> 0x33); + uint64_t x372 = (x370 & 0x7ffffffffffff); + uint64_t x373 = (x371 + x360); + uint64_t x374 = (x366 + x270); + uint64_t x375 = (x363 + x267); + uint64_t x376 = (x373 + x277); + uint64_t x377 = (x372 + x276); + uint64_t x378 = (x369 + x273); + uint128_t x379 = ((uint128_t)x347 * x378); + uint128_t x380 = (((uint128_t)x347 * x377) + ((uint128_t)x346 * x378)); + uint128_t x381 = ((((uint128_t)x347 * x376) + ((uint128_t)x345 * x378)) + ((uint128_t)x346 * x377)); + uint128_t x382 = (((((uint128_t)x347 * x375) + ((uint128_t)x344 * x378)) + ((uint128_t)x346 * x376)) + ((uint128_t)x345 * x377)); + uint128_t x383 = ((((((uint128_t)x347 * x374) + ((uint128_t)x343 * x378)) + ((uint128_t)x344 * x377)) + ((uint128_t)x346 * x375)) + ((uint128_t)x345 * x376)); + uint64_t x384 = (x343 * 0x13); + uint64_t x385 = (x346 * 0x13); + uint64_t x386 = (x345 * 0x13); + uint64_t x387 = (x344 * 0x13); + uint128_t x388 = ((((x379 + ((uint128_t)x384 * x377)) + ((uint128_t)x385 * x374)) + ((uint128_t)x386 * x375)) + ((uint128_t)x387 * x376)); + uint128_t x389 = (((x380 + ((uint128_t)x384 * x376)) + ((uint128_t)x386 * x374)) + ((uint128_t)x387 * x375)); + uint128_t x390 = ((x381 + ((uint128_t)x384 * x375)) + ((uint128_t)x387 * x374)); + uint128_t x391 = (x382 + ((uint128_t)x384 * x374)); uint64_t x392 = (uint64_t) (x388 >> 0x33); - uint64_t x393 = (uint64_t) x388 & 0x7ffffffffffff; - uint128_t x394 = x392 + x389; + uint64_t x393 = ((uint64_t)x388 & 0x7ffffffffffff); + uint128_t x394 = (x392 + x389); uint64_t x395 = (uint64_t) (x394 >> 0x33); - uint64_t x396 = (uint64_t) x394 & 0x7ffffffffffff; - uint128_t x397 = x395 + x390; + uint64_t x396 = ((uint64_t)x394 & 0x7ffffffffffff); + uint128_t x397 = (x395 + x390); uint64_t x398 = (uint64_t) (x397 >> 0x33); - uint64_t x399 = (uint64_t) x397 & 0x7ffffffffffff; - uint128_t x400 = x398 + x391; + uint64_t x399 = ((uint64_t)x397 & 0x7ffffffffffff); + uint128_t x400 = (x398 + x391); uint64_t x401 = (uint64_t) (x400 >> 0x33); - uint64_t x402 = (uint64_t) x400 & 0x7ffffffffffff; - uint128_t x403 = x401 + x383; + uint64_t x402 = ((uint64_t)x400 & 0x7ffffffffffff); + uint128_t x403 = (x401 + x383); uint64_t x404 = (uint64_t) (x403 >> 0x33); - uint64_t x405 = (uint64_t) x403 & 0x7ffffffffffff; - uint64_t x406 = x393 + 0x13 * x404; - uint64_t x407 = x406 >> 0x33; - uint64_t x408 = x406 & 0x7ffffffffffff; - uint64_t x409 = x407 + x396; - uint64_t x410 = x409 >> 0x33; - uint64_t x411 = x409 & 0x7ffffffffffff; - uint64_t x412 = x410 + x399; + uint64_t x405 = ((uint64_t)x403 & 0x7ffffffffffff); + uint64_t x406 = (x393 + (0x13 * x404)); + uint64_t x407 = (x406 >> 0x33); + uint64_t x408 = (x406 & 0x7ffffffffffff); + uint64_t x409 = (x407 + x396); + uint64_t x410 = (x409 >> 0x33); + uint64_t x411 = (x409 & 0x7ffffffffffff); + uint64_t x412 = (x410 + x399); return (Return x335, Return x332, Return x342, Return x341, Return x338, (Return x405, Return x402, Return x412, Return x411, Return x408), (Return x174, Return x171, Return x181, Return x180, Return x177, (Return x239, Return x236, Return x246, Return x245, Return x242)))) (x, (x0, x1), (x2, x3))%core in (let (a0, b0) := a in |