VADDPD X30, X11, X28        // 6201a50858e6
	VADDPD X12, X29, X28        // 6241950058e4
	VADDPD X30, X29, X28        // 6201950058e6
	VADDPD (AX), X29, X0        // 62f195005800
	VADDPD (AX), X1, X28        // 6261f5085820
	VADDPD (AX), X29, X28       // 626195005820
	VADDPD (AX), X29, X10       // 627195005810
	VADDPD (AX), X10, X28       // 6261ad085820
	VADDPD (CX)(AX*1), X29, X0  // 62f19500580401

	p384CmovznzU64(&x28, p384Uint1(x26), x15, x3)
	var x29 uint64
	p384CmovznzU64(&x29, p384Uint1(x26), x17, x5)
	var x30 uint64
	p384CmovznzU64(&x30, p384Uint1(x26), x19, x7)
	var x31 uint64
	p384CmovznzU64(&x31, p384Uint1(x26), x21, x9)
	var x32 uint64
	p384CmovznzU64(&x32, p384Uint1(x26), x23, x11)
	out1[0] = x27
	out1[1] = x28
	out1[2] = x29
	out1[3] = x30
	out1[4] = x31
	out1[5] = x32
}