#include <stdint.h>
#include "uint128.h"
void
mul_128(uint64_t a, uint64_t b, uint64_t *cL, uint64_t *cH)
{
uint64_t a0 = a & 0xFFFFFFFF;
uint64_t a1 = a >> 32;
uint64_t b0 = b & 0xFFFFFFFF;
uint64_t b1 = b >> 32;
uint64_t ab00 = a0 * b0;
uint64_t ab01 = a0 * b1;
uint64_t ab10 = a1 * b0;
uint64_t ab11 = a1 * b1;
*cL = (ab00 >> 32) + (ab01 & 0xFFFFFFFF) + (ab10 & 0xFFFFFFFF);
*cH = (*cL >> 32) + (ab01 >> 32) + (ab10 >> 32) + ab11;
*cL = (*cL << 32) + (ab00 & 0xFFFFFFFF);
}
/*
void div_128(uint64_t a, uint64_t bL, uint64_t bH, uint64_t *cL, uint64_t *cH,
uint64_t *r)
{
// TODO
}
*/