pure void  mul64x64_128(ulong a, ulong b, ref ulong[2] res);