x41, x40 = bits.Mul64(x30, 0xffffffff00000000)
	var x42 uint64
	var x43 uint64
	x43, x42 = bits.Mul64(x30, 0xffffffff)
	var x44 uint64
	var x45 uint64
	x44, x45 = bits.Add64(x43, x40, uint64(0x0))
	var x46 uint64
	var x47 uint64
	x46, x47 = bits.Add64(x41, x38, uint64(p384Uint1(x45)))
	var x48 uint64
	var x49 uint64
	x48, x49 = bits.Add64(x39, x36, uint64(p384Uint1(x47)))
	var x50 uint64
	var x51 uint64