diff options
Diffstat (limited to 'src/Specific/X2555/C128/ladderstepDisplay.log')
| -rw-r--r-- | src/Specific/X2555/C128/ladderstepDisplay.log | 214 |
1 files changed, 214 insertions, 0 deletions
diff --git a/src/Specific/X2555/C128/ladderstepDisplay.log b/src/Specific/X2555/C128/ladderstepDisplay.log new file mode 100644 index 000000000..d6c2ec14d --- /dev/null +++ b/src/Specific/X2555/C128/ladderstepDisplay.log @@ -0,0 +1,214 @@ +λ x x0 x1 x2 x3 : Synthesis.P.feW, +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; + uint128_t x39 = x27 + x31; + uint128_t x40 = x28 + x32; + uint128_t x41 = x26 + x30; + uint128_t x42 = 0x3ffffffffffffffffffffeL + x27 - x31; + uint128_t x43 = 0x3ffffffffffffffffffffeL + x28 - x32; + uint128_t x44 = 0x3ffffffffffffffffffff6L + x26 - x30; + uint256_t x45 = (uint256_t) x41 * x36 + ((uint256_t) x40 * x37 + (uint256_t) x39 * x38); + uint256_t x46 = (uint256_t) x41 * x37 + (uint256_t) x40 * x38 + 0x5 * ((uint256_t) x39 * x36); + uint256_t x47 = (uint256_t) x41 * x38 + 0x5 * ((uint256_t) x40 * x36 + (uint256_t) x39 * x37); + uint128_t x48 = (uint128_t) (x47 >> 0x55); + uint128_t x49 = (uint128_t) x47 & 0x1fffffffffffffffffffffL; + uint256_t x50 = x48 + x46; + uint128_t x51 = (uint128_t) (x50 >> 0x55); + uint128_t x52 = (uint128_t) x50 & 0x1fffffffffffffffffffffL; + uint256_t x53 = x51 + x45; + uint128_t x54 = (uint128_t) (x53 >> 0x55); + uint128_t x55 = (uint128_t) x53 & 0x1fffffffffffffffffffffL; + uint128_t x56 = x49 + 0x5 * x54; + uint128_t x57 = x56 >> 0x55; + uint128_t x58 = x56 & 0x1fffffffffffffffffffffL; + uint128_t x59 = x57 + x52; + uint128_t x60 = x59 >> 0x55; + uint128_t x61 = x59 & 0x1fffffffffffffffffffffL; + uint128_t x62 = x60 + x55; + uint256_t x63 = (uint256_t) x35 * x42 + ((uint256_t) x34 * x43 + (uint256_t) x33 * x44); + uint256_t x64 = (uint256_t) x35 * x43 + (uint256_t) x34 * x44 + 0x5 * ((uint256_t) x33 * x42); + uint256_t x65 = (uint256_t) x35 * x44 + 0x5 * ((uint256_t) x34 * x42 + (uint256_t) x33 * x43); + uint128_t x66 = (uint128_t) (x65 >> 0x55); + uint128_t x67 = (uint128_t) x65 & 0x1fffffffffffffffffffffL; + uint256_t x68 = x66 + x64; + uint128_t x69 = (uint128_t) (x68 >> 0x55); + uint128_t x70 = (uint128_t) x68 & 0x1fffffffffffffffffffffL; + uint256_t x71 = x69 + x63; + uint128_t x72 = (uint128_t) (x71 >> 0x55); + uint128_t x73 = (uint128_t) x71 & 0x1fffffffffffffffffffffL; + uint128_t x74 = x67 + 0x5 * x72; + uint128_t x75 = x74 >> 0x55; + uint128_t x76 = x74 & 0x1fffffffffffffffffffffL; + uint128_t x77 = x75 + x70; + uint128_t x78 = x77 >> 0x55; + uint128_t x79 = x77 & 0x1fffffffffffffffffffffL; + uint128_t x80 = x78 + x73; + uint128_t x81 = x62 + x80; + uint128_t x82 = x61 + x79; + uint128_t x83 = x58 + x76; + uint128_t x84 = 0x3ffffffffffffffffffffeL + x62 - x80; + uint128_t x85 = 0x3ffffffffffffffffffffeL + x61 - x79; + uint128_t x86 = 0x3ffffffffffffffffffff6L + x58 - x76; + uint256_t x87 = (uint256_t) x83 * x81 + ((uint256_t) x82 * x82 + (uint256_t) x81 * x83); + uint256_t x88 = (uint256_t) x83 * x82 + (uint256_t) x82 * x83 + 0x5 * ((uint256_t) x81 * x81); + uint256_t x89 = (uint256_t) x83 * x83 + 0x5 * ((uint256_t) x82 * x81 + (uint256_t) x81 * x82); + uint128_t x90 = (uint128_t) (x89 >> 0x55); + uint128_t x91 = (uint128_t) x89 & 0x1fffffffffffffffffffffL; + uint256_t x92 = x90 + x88; + uint128_t x93 = (uint128_t) (x92 >> 0x55); + uint128_t x94 = (uint128_t) x92 & 0x1fffffffffffffffffffffL; + uint256_t x95 = x93 + x87; + uint128_t x96 = (uint128_t) (x95 >> 0x55); + uint128_t x97 = (uint128_t) x95 & 0x1fffffffffffffffffffffL; + uint128_t x98 = x91 + 0x5 * x96; + uint128_t x99 = x98 >> 0x55; + uint128_t x100 = x98 & 0x1fffffffffffffffffffffL; + uint128_t x101 = x99 + x94; + uint128_t x102 = x101 >> 0x55; + uint128_t x103 = x101 & 0x1fffffffffffffffffffffL; + uint128_t x104 = x102 + x97; + uint256_t x105 = (uint256_t) x86 * x84 + ((uint256_t) x85 * x85 + (uint256_t) x84 * x86); + uint256_t x106 = (uint256_t) x86 * x85 + (uint256_t) x85 * x86 + 0x5 * ((uint256_t) x84 * x84); + uint256_t x107 = (uint256_t) x86 * x86 + 0x5 * ((uint256_t) x85 * x84 + (uint256_t) x84 * x85); + uint128_t x108 = (uint128_t) (x107 >> 0x55); + uint128_t x109 = (uint128_t) x107 & 0x1fffffffffffffffffffffL; + uint256_t x110 = x108 + x106; + uint128_t x111 = (uint128_t) (x110 >> 0x55); + uint128_t x112 = (uint128_t) x110 & 0x1fffffffffffffffffffffL; + uint256_t x113 = x111 + x105; + uint128_t x114 = (uint128_t) (x113 >> 0x55); + uint128_t x115 = (uint128_t) x113 & 0x1fffffffffffffffffffffL; + uint128_t x116 = x109 + 0x5 * x114; + uint128_t x117 = x116 >> 0x55; + uint128_t x118 = x116 & 0x1fffffffffffffffffffffL; + uint128_t x119 = x117 + x112; + uint128_t x120 = x119 >> 0x55; + uint128_t x121 = x119 & 0x1fffffffffffffffffffffL; + uint128_t x122 = x120 + x115; + uint256_t x123 = (uint256_t) x118 * x11 + ((uint256_t) x121 * x12 + (uint256_t) x122 * x10); + uint256_t x124 = (uint256_t) x118 * x12 + (uint256_t) x121 * x10 + 0x5 * ((uint256_t) x122 * x11); + uint256_t x125 = (uint256_t) x118 * x10 + 0x5 * ((uint256_t) x121 * x11 + (uint256_t) x122 * x12); + uint128_t x126 = (uint128_t) (x125 >> 0x55); + uint128_t x127 = (uint128_t) x125 & 0x1fffffffffffffffffffffL; + uint256_t x128 = x126 + x124; + uint128_t x129 = (uint128_t) (x128 >> 0x55); + uint128_t x130 = (uint128_t) x128 & 0x1fffffffffffffffffffffL; + uint256_t x131 = x129 + x123; + uint128_t x132 = (uint128_t) (x131 >> 0x55); + uint128_t x133 = (uint128_t) x131 & 0x1fffffffffffffffffffffL; + uint128_t x134 = x127 + 0x5 * x132; + uint128_t x135 = x134 >> 0x55; + uint128_t x136 = x134 & 0x1fffffffffffffffffffffL; + uint128_t x137 = x135 + x130; + uint128_t x138 = x137 >> 0x55; + uint128_t x139 = x137 & 0x1fffffffffffffffffffffL; + uint128_t x140 = x138 + x133; + uint256_t x141 = (uint256_t) x35 * x33 + ((uint256_t) x34 * x34 + (uint256_t) x33 * x35); + uint256_t x142 = (uint256_t) x35 * x34 + (uint256_t) x34 * x35 + 0x5 * ((uint256_t) x33 * x33); + uint256_t x143 = (uint256_t) x35 * x35 + 0x5 * ((uint256_t) x34 * x33 + (uint256_t) x33 * x34); + uint128_t x144 = (uint128_t) (x143 >> 0x55); + 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 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) x38 * x36 + ((uint256_t) x37 * x37 + (uint256_t) x36 * x38); + uint256_t x160 = (uint256_t) x38 * x37 + (uint256_t) x37 * x38 + 0x5 * ((uint256_t) x36 * x36); + uint256_t x161 = (uint256_t) x38 * x38 + 0x5 * ((uint256_t) x37 * x36 + (uint256_t) x36 * x37); + uint128_t x162 = (uint128_t) (x161 >> 0x55); + 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 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; + uint256_t x177 = (uint256_t) x154 * x176 + ((uint256_t) x157 * x175 + (uint256_t) x158 * x172); + uint256_t x178 = (uint256_t) x154 * x175 + (uint256_t) x157 * x172 + 0x5 * ((uint256_t) x158 * x176); + uint256_t x179 = (uint256_t) x154 * x172 + 0x5 * ((uint256_t) x157 * x176 + (uint256_t) x158 * x175); + uint128_t x180 = (uint128_t) (x179 >> 0x55); + uint128_t x181 = (uint128_t) x179 & 0x1fffffffffffffffffffffL; + uint256_t x182 = x180 + x178; + uint128_t x183 = (uint128_t) (x182 >> 0x55); + uint128_t x184 = (uint128_t) x182 & 0x1fffffffffffffffffffffL; + uint256_t x185 = x183 + x177; + uint128_t x186 = (uint128_t) (x185 >> 0x55); + uint128_t x187 = (uint128_t) x185 & 0x1fffffffffffffffffffffL; + uint128_t x188 = x181 + 0x5 * x186; + uint128_t x189 = x188 >> 0x55; + uint128_t x190 = x188 & 0x1fffffffffffffffffffffL; + uint128_t x191 = x189 + x184; + uint128_t x192 = x191 >> 0x55; + uint128_t x193 = x191 & 0x1fffffffffffffffffffffL; + uint128_t x194 = x192 + x187; + uint128_t x195 = 0x3ffffffffffffffffffffeL + x158 - x176; + uint128_t x196 = 0x3ffffffffffffffffffffeL + x157 - x175; + uint128_t x197 = 0x3ffffffffffffffffffff6L + x154 - x172; + uint128_t x198 = x195 * 0x1db41; + uint128_t x199 = x196 * 0x1db41; + uint128_t x200 = x197 * 0x1db41; + uint128_t x201 = x200 >> 0x55; + uint128_t x202 = x200 & 0x1fffffffffffffffffffffL; + uint128_t x203 = x201 + x199; + uint128_t x204 = x203 >> 0x55; + uint128_t x205 = x203 & 0x1fffffffffffffffffffffL; + uint128_t x206 = x204 + x198; + uint128_t x207 = x206 >> 0x55; + uint128_t x208 = x206 & 0x1fffffffffffffffffffffL; + uint128_t x209 = x202 + 0x5 * x207; + uint128_t x210 = x209 >> 0x55; + uint128_t x211 = x209 & 0x1fffffffffffffffffffffL; + uint128_t x212 = x210 + x205; + uint128_t x213 = x212 >> 0x55; + uint128_t x214 = x212 & 0x1fffffffffffffffffffffL; + uint128_t x215 = x213 + x208; + uint128_t x216 = x215 + x158; + uint128_t x217 = x214 + x157; + uint128_t x218 = x211 + x154; + uint256_t x219 = (uint256_t) x197 * x216 + ((uint256_t) x196 * x217 + (uint256_t) x195 * x218); + uint256_t x220 = (uint256_t) x197 * x217 + (uint256_t) x196 * x218 + 0x5 * ((uint256_t) x195 * x216); + uint256_t x221 = (uint256_t) x197 * x218 + 0x5 * ((uint256_t) x196 * x216 + (uint256_t) x195 * x217); + uint128_t x222 = (uint128_t) (x221 >> 0x55); + uint128_t x223 = (uint128_t) x221 & 0x1fffffffffffffffffffffL; + uint256_t x224 = x222 + x220; + uint128_t x225 = (uint128_t) (x224 >> 0x55); + uint128_t x226 = (uint128_t) x224 & 0x1fffffffffffffffffffffL; + uint256_t x227 = x225 + x219; + uint128_t x228 = (uint128_t) (x227 >> 0x55); + uint128_t x229 = (uint128_t) x227 & 0x1fffffffffffffffffffffL; + uint128_t x230 = x223 + 0x5 * x228; + uint128_t x231 = x230 >> 0x55; + uint128_t x232 = x230 & 0x1fffffffffffffffffffffL; + uint128_t x233 = x231 + x226; + uint128_t x234 = x233 >> 0x55; + uint128_t x235 = x233 & 0x1fffffffffffffffffffffL; + uint128_t x236 = x234 + x229; + return (Return x194, Return x193, Return x190, (Return x236, Return x235, Return x232), (Return x104, Return x103, Return x100, (Return x140, Return x139, Return x136)))) +(x, (x0, x1), (x2, x3))%core in +(let (a0, b0) := a in +(a0, b0), let (a0, b0) := b in +(a0, b0))%core + : Synthesis.P.feW → Synthesis.P.feW → Synthesis.P.feW → Synthesis.P.feW → Synthesis.P.feW → Synthesis.P.feW * Synthesis.P.feW * (Synthesis.P.feW * Synthesis.P.feW) |