VCVTQQ2PD X13, K3, X30                             // 6241fe0be6f5
	VCVTQQ2PD X6, K3, X30                              // 6261fe0be6f6
	VCVTQQ2PD X12, K3, X30                             // 6241fe0be6f4
	VCVTQQ2PD 17(SP)(BP*1), K3, X30                    // 6261fe0be6b42c11000000
	VCVTQQ2PD -7(CX)(DX*8), K3, X30                    // 6261fe0be6b4d1f9ffffff

	var x28 uint64
	x27, x28 = bits.Sub64(x9, 0xffffffffffffffff, uint64(p521Uint1(x26)))
	var x29 uint64
	var x30 uint64
	x29, x30 = bits.Sub64(x11, 0xffffffffffffffff, uint64(p521Uint1(x28)))
	var x31 uint64
	var x32 uint64
	x31, x32 = bits.Sub64(x13, 0xffffffffffffffff, uint64(p521Uint1(x30)))
	var x33 uint64
	var x34 uint64
	x33, x34 = bits.Sub64(x15, 0xffffffffffffffff, uint64(p521Uint1(x32)))

	VPADDSB -15(R14)(R15*4), Z6, K7, Z14               // 62114d4fecb4bef1ffffff or 6211cd4fecb4bef1ffffff
	VPADDSW X6, X13, K7, X30                           // 6261150fedf6 or 6261950fedf6
	VPADDSW 99(R15)(R15*2), X13, K7, X30               // 6201150fedb47f63000000 or 6201950fedb47f63000000
	VPADDSW -7(DI), X13, K7, X30                       // 6261150fedb7f9ffffff or 6261950fedb7f9ffffff