kris
/
SIDH_p751
1
0
Vork 0
Code Kwesties 0 Pull-aanvragen 0 Publicaties 0 Wiki Activiteit
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
45 Commits
14 Branches
653 KiB
 
 
 
Tree: 8045da3721
Branches Labels
${ item.name }
Maak branch ${ searchTerm }
van '8045da3721'
${ noResults }
SIDH_p751/field_amd64.s

2378 regels
38 KiB
Ruw Blame Geschiedenis 

  1. #include "textflag.h"

  2. 

  3. // p751 + 1

  4. #define P751P1_5   $0xEEB0000000000000

  5. #define P751P1_6   $0xE3EC968549F878A8

  6. #define P751P1_7   $0xDA959B1A13F7CC76

  7. #define P751P1_8   $0x084E9867D6EBE876

  8. #define P751P1_9   $0x8562B5045CB25748

  9. #define P751P1_10  $0x0E12909F97BADC66

  10. #define P751P1_11  $0x00006FE5D541F71C

  11. 

  12. #define P751_0     $0xFFFFFFFFFFFFFFFF

  13. #define P751_5     $0xEEAFFFFFFFFFFFFF

  14. #define P751_6     $0xE3EC968549F878A8

  15. #define P751_7     $0xDA959B1A13F7CC76

  16. #define P751_8     $0x084E9867D6EBE876

  17. #define P751_9     $0x8562B5045CB25748

  18. #define P751_10    $0x0E12909F97BADC66

  19. #define P751_11    $0x00006FE5D541F71C

  20. 

  21. #define P751X2_0   $0xFFFFFFFFFFFFFFFE

  22. #define P751X2_1   $0xFFFFFFFFFFFFFFFF

  23. #define P751X2_5   $0xDD5FFFFFFFFFFFFF

  24. #define P751X2_6   $0xC7D92D0A93F0F151

  25. #define P751X2_7   $0xB52B363427EF98ED

  26. #define P751X2_8   $0x109D30CFADD7D0ED

  27. #define P751X2_9   $0x0AC56A08B964AE90

  28. #define P751X2_10  $0x1C25213F2F75B8CD

  29. #define P751X2_11  $0x0000DFCBAA83EE38

  30. 

  31. // The MSR code uses these registers for parameter passing.  Keep using

  32. // them to avoid significant code changes.  This means that when the Go

  33. // assembler does something strange, we can diff the machine code

  34. // against a different assembler to find out what Go did.

  35. 

  36. #define REG_P1 DI

  37. #define REG_P2 SI

  38. #define REG_P3 DX

  39. 

  40. // We can't write MOVQ $0, AX because Go's assembler incorrectly

  41. // optimizes this to XOR AX, AX, which clobbers the carry flags.

  42. //

  43. // This bug was defined to be "correct" behaviour (cf.

  44. // https://github.com/golang/go/issues/12405 ) by declaring that the MOV

  45. // pseudo-instruction clobbers flags, although this fact is mentioned

  46. // nowhere in the documentation for the Go assembler.

  47. //

  48. // Defining MOVQ to clobber flags has the effect that it is never safe

  49. // to interleave MOVQ with ADCQ and SBBQ instructions.  Since this is

  50. // required to write a carry chain longer than registers' working set,

  51. // all of the below code therefore relies on the unspecified and

  52. // undocumented behaviour that MOV won't clobber flags, except in the

  53. // case of the above-mentioned bug.

  54. //

  55. // However, there's also no specification of which instructions

  56. // correspond to machine instructions, and which are

  57. // pseudo-instructions (i.e., no specification of what the assembler

  58. // actually does), so this doesn't seem much worse than usual.

  59. //

  60. // Avoid the bug by dropping the bytes for `mov eax, 0` in directly:

  61. 

  62. #define ZERO_AX_WITHOUT_CLOBBERING_FLAGS BYTE	$0xB8; BYTE $0; BYTE $0; BYTE $0; BYTE $0;

  63. 

  64. TEXT ·fp751StrongReduce(SB), NOSPLIT, $0-8

  65. 	MOVQ	x+0(FP), REG_P1

  66. 

  67. 	// Zero AX for later use:

  68. 	XORQ	AX, AX

  69. 

  70. 	// Load p into registers:

  71. 	MOVQ	P751_0, R8

  72. 	// P751_{1,2,3,4} = P751_0, so reuse R8

  73. 	MOVQ	P751_5, R9

  74. 	MOVQ	P751_6, R10

  75. 	MOVQ	P751_7, R11

  76. 	MOVQ	P751_8, R12

  77. 	MOVQ	P751_9, R13

  78. 	MOVQ	P751_10, R14

  79. 	MOVQ	P751_11, R15

  80. 

  81. 	// Set x <- x - p

  82. 	SUBQ	R8, (REG_P1)

  83. 	SBBQ	R8, (8)(REG_P1)

  84. 	SBBQ	R8, (16)(REG_P1)

  85. 	SBBQ	R8, (24)(REG_P1)

  86. 	SBBQ	R8, (32)(REG_P1)

  87. 	SBBQ	R9, (40)(REG_P1)

  88. 	SBBQ	R10, (48)(REG_P1)

  89. 	SBBQ	R11, (56)(REG_P1)

  90. 	SBBQ	R12, (64)(REG_P1)

  91. 	SBBQ	R13, (72)(REG_P1)

  92. 	SBBQ	R14, (80)(REG_P1)

  93. 	SBBQ    R15, (88)(REG_P1)

  94. 

  95. 	// Save carry flag indicating x-p < 0 as a mask in AX

  96. 	SBBQ	$0, AX

  97. 

  98. 	// Conditionally add p to x if x-p < 0

  99. 	ANDQ	AX, R8

  100. 	ANDQ	AX, R9

  101. 	ANDQ	AX, R10

  102. 	ANDQ	AX, R11

  103. 	ANDQ	AX, R12

  104. 	ANDQ	AX, R13

  105. 	ANDQ	AX, R14

  106. 	ANDQ	AX, R15

  107. 

  108. 	ADDQ	R8, (REG_P1)

  109. 	ADCQ	R8, (8)(REG_P1)

  110. 	ADCQ	R8, (16)(REG_P1)

  111. 	ADCQ	R8, (24)(REG_P1)

  112. 	ADCQ	R8, (32)(REG_P1)

  113. 	ADCQ	R9, (40)(REG_P1)

  114. 	ADCQ	R10, (48)(REG_P1)

  115. 	ADCQ	R11, (56)(REG_P1)

  116. 	ADCQ	R12, (64)(REG_P1)

  117. 	ADCQ	R13, (72)(REG_P1)

  118. 	ADCQ	R14, (80)(REG_P1)

  119. 	ADCQ    R15, (88)(REG_P1)

  120. 

  121. 	RET

  122. 

  123. TEXT ·fp751ConditionalSwap(SB), NOSPLIT, $0-17

  124. 

  125. 	MOVQ	x+0(FP), REG_P1

  126. 	MOVQ	y+8(FP), REG_P2

  127. 	MOVB	choice+16(FP), AL	// AL = 0 or 1

  128. 	MOVBLZX	AL, AX			// AX = 0 or 1

  129. 	NEGQ	AX			// RAX = 0x00..00 or 0xff..ff

  130. 

  131. 	MOVQ	(0*8)(REG_P1), BX	// BX = x[0]

  132. 	MOVQ 	(0*8)(REG_P2), CX	// CX = y[0]

  133. 	MOVQ	CX, DX			// DX = y[0]

  134. 	XORQ	BX, DX			// DX = y[0] ^ x[0]

  135. 	ANDQ	AX, DX			// DX = (y[0] ^ x[0]) & mask

  136. 	XORQ	DX, BX			// BX = (y[0] ^ x[0]) & mask) ^ x[0] = x[0] or y[0]

  137. 	XORQ	DX, CX			// CX = (y[0] ^ x[0]) & mask) ^ y[0] = y[0] or x[0]

  138. 	MOVQ	BX, (0*8)(REG_P1)

  139. 	MOVQ	CX, (0*8)(REG_P2)

  140. 

  141. 	MOVQ	(1*8)(REG_P1), BX

  142. 	MOVQ 	(1*8)(REG_P2), CX

  143. 	MOVQ	CX, DX

  144. 	XORQ	BX, DX

  145. 	ANDQ	AX, DX

  146. 	XORQ	DX, BX

  147. 	XORQ	DX, CX

  148. 	MOVQ	BX, (1*8)(REG_P1)

  149. 	MOVQ	CX, (1*8)(REG_P2)

  150. 

  151. 	MOVQ	(2*8)(REG_P1), BX

  152. 	MOVQ 	(2*8)(REG_P2), CX

  153. 	MOVQ	CX, DX

  154. 	XORQ	BX, DX

  155. 	ANDQ	AX, DX

  156. 	XORQ	DX, BX

  157. 	XORQ	DX, CX

  158. 	MOVQ	BX, (2*8)(REG_P1)

  159. 	MOVQ	CX, (2*8)(REG_P2)

  160. 

  161. 	MOVQ	(3*8)(REG_P1), BX

  162. 	MOVQ 	(3*8)(REG_P2), CX

  163. 	MOVQ	CX, DX

  164. 	XORQ	BX, DX

  165. 	ANDQ	AX, DX

  166. 	XORQ	DX, BX

  167. 	XORQ	DX, CX

  168. 	MOVQ	BX, (3*8)(REG_P1)

  169. 	MOVQ	CX, (3*8)(REG_P2)

  170. 

  171. 	MOVQ	(4*8)(REG_P1), BX

  172. 	MOVQ 	(4*8)(REG_P2), CX

  173. 	MOVQ	CX, DX

  174. 	XORQ	BX, DX

  175. 	ANDQ	AX, DX

  176. 	XORQ	DX, BX

  177. 	XORQ	DX, CX

  178. 	MOVQ	BX, (4*8)(REG_P1)

  179. 	MOVQ	CX, (4*8)(REG_P2)

  180. 

  181. 	MOVQ	(5*8)(REG_P1), BX

  182. 	MOVQ 	(5*8)(REG_P2), CX

  183. 	MOVQ	CX, DX

  184. 	XORQ	BX, DX

  185. 	ANDQ	AX, DX

  186. 	XORQ	DX, BX

  187. 	XORQ	DX, CX

  188. 	MOVQ	BX, (5*8)(REG_P1)

  189. 	MOVQ	CX, (5*8)(REG_P2)

  190. 

  191. 	MOVQ	(6*8)(REG_P1), BX

  192. 	MOVQ 	(6*8)(REG_P2), CX

  193. 	MOVQ	CX, DX

  194. 	XORQ	BX, DX

  195. 	ANDQ	AX, DX

  196. 	XORQ	DX, BX

  197. 	XORQ	DX, CX

  198. 	MOVQ	BX, (6*8)(REG_P1)

  199. 	MOVQ	CX, (6*8)(REG_P2)

  200. 

  201. 	MOVQ	(7*8)(REG_P1), BX

  202. 	MOVQ 	(7*8)(REG_P2), CX

  203. 	MOVQ	CX, DX

  204. 	XORQ	BX, DX

  205. 	ANDQ	AX, DX

  206. 	XORQ	DX, BX

  207. 	XORQ	DX, CX

  208. 	MOVQ	BX, (7*8)(REG_P1)

  209. 	MOVQ	CX, (7*8)(REG_P2)

  210. 

  211. 	MOVQ	(8*8)(REG_P1), BX

  212. 	MOVQ 	(8*8)(REG_P2), CX

  213. 	MOVQ	CX, DX

  214. 	XORQ	BX, DX

  215. 	ANDQ	AX, DX

  216. 	XORQ	DX, BX

  217. 	XORQ	DX, CX

  218. 	MOVQ	BX, (8*8)(REG_P1)

  219. 	MOVQ	CX, (8*8)(REG_P2)

  220. 

  221. 	MOVQ	(9*8)(REG_P1), BX

  222. 	MOVQ 	(9*8)(REG_P2), CX

  223. 	MOVQ	CX, DX

  224. 	XORQ	BX, DX

  225. 	ANDQ	AX, DX

  226. 	XORQ	DX, BX

  227. 	XORQ	DX, CX

  228. 	MOVQ	BX, (9*8)(REG_P1)

  229. 	MOVQ	CX, (9*8)(REG_P2)

  230. 

  231. 	MOVQ	(10*8)(REG_P1), BX

  232. 	MOVQ 	(10*8)(REG_P2), CX

  233. 	MOVQ	CX, DX

  234. 	XORQ	BX, DX

  235. 	ANDQ	AX, DX

  236. 	XORQ	DX, BX

  237. 	XORQ	DX, CX

  238. 	MOVQ	BX, (10*8)(REG_P1)

  239. 	MOVQ	CX, (10*8)(REG_P2)

  240. 

  241. 	MOVQ	(11*8)(REG_P1), BX

  242. 	MOVQ 	(11*8)(REG_P2), CX

  243. 	MOVQ	CX, DX

  244. 	XORQ	BX, DX

  245. 	ANDQ	AX, DX

  246. 	XORQ	DX, BX

  247. 	XORQ	DX, CX

  248. 	MOVQ	BX, (11*8)(REG_P1)

  249. 	MOVQ	CX, (11*8)(REG_P2)

  250. 

  251. 	RET

  252. 

  253. TEXT ·fp751ConditionalAssign(SB), NOSPLIT, $0-25

  254. 

  255. 	MOVQ	z+0(FP), REG_P3

  256. 	MOVQ	x+8(FP), REG_P1

  257. 	MOVQ	y+16(FP), REG_P2

  258. 	MOVB	choice+24(FP), AL	// AL = 0 or 1

  259. 	MOVBLZX	AL, AX			// AX = 0 or 1

  260. 	NEGQ	AX			// RAX = 0x00..00 or 0xff..ff

  261. 

  262. 	MOVQ	(0*8)(REG_P1), BX	// BX = x[0]

  263. 	MOVQ 	(0*8)(REG_P2), CX	// CX = y[0]

  264. 	XORQ	BX, CX			// CX = y[0] ^ x[0]

  265. 	ANDQ	AX, CX			// CX = (y[0] ^ x[0]) & mask

  266. 	XORQ	BX, CX			// CX = (y[0] ^ x[0]) & mask) ^ x[0]

  267. 	MOVQ	CX, (0*8)(REG_P3)	//    = x[0] or y[0]

  268. 

  269. 	MOVQ	(1*8)(REG_P1), BX

  270. 	MOVQ 	(1*8)(REG_P2), CX

  271. 	XORQ	BX, CX

  272. 	ANDQ	AX, CX

  273. 	XORQ	BX, CX

  274. 	MOVQ	CX, (1*8)(REG_P3)

  275. 

  276. 	MOVQ	(2*8)(REG_P1), BX

  277. 	MOVQ 	(2*8)(REG_P2), CX

  278. 	XORQ	BX, CX

  279. 	ANDQ	AX, CX

  280. 	XORQ	BX, CX

  281. 	MOVQ	CX, (2*8)(REG_P3)

  282. 

  283. 	MOVQ	(3*8)(REG_P1), BX

  284. 	MOVQ 	(3*8)(REG_P2), CX

  285. 	XORQ	BX, CX

  286. 	ANDQ	AX, CX

  287. 	XORQ	BX, CX

  288. 	MOVQ	CX, (3*8)(REG_P3)

  289. 

  290. 	MOVQ	(4*8)(REG_P1), BX

  291. 	MOVQ 	(4*8)(REG_P2), CX

  292. 	XORQ	BX, CX

  293. 	ANDQ	AX, CX

  294. 	XORQ	BX, CX

  295. 	MOVQ	CX, (4*8)(REG_P3)

  296. 

  297. 	MOVQ	(5*8)(REG_P1), BX

  298. 	MOVQ 	(5*8)(REG_P2), CX

  299. 	XORQ	BX, CX

  300. 	ANDQ	AX, CX

  301. 	XORQ	BX, CX

  302. 	MOVQ	CX, (5*8)(REG_P3)

  303. 

  304. 	MOVQ	(6*8)(REG_P1), BX

  305. 	MOVQ 	(6*8)(REG_P2), CX

  306. 	XORQ	BX, CX

  307. 	ANDQ	AX, CX

  308. 	XORQ	BX, CX

  309. 	MOVQ	CX, (6*8)(REG_P3)

  310. 

  311. 	MOVQ	(7*8)(REG_P1), BX

  312. 	MOVQ 	(7*8)(REG_P2), CX

  313. 	XORQ	BX, CX

  314. 	ANDQ	AX, CX

  315. 	XORQ	BX, CX

  316. 	MOVQ	CX, (7*8)(REG_P3)

  317. 

  318. 	MOVQ	(8*8)(REG_P1), BX

  319. 	MOVQ 	(8*8)(REG_P2), CX

  320. 	XORQ	BX, CX

  321. 	ANDQ	AX, CX

  322. 	XORQ	BX, CX

  323. 	MOVQ	CX, (8*8)(REG_P3)

  324. 

  325. 	MOVQ	(9*8)(REG_P1), BX

  326. 	MOVQ 	(9*8)(REG_P2), CX

  327. 	XORQ	BX, CX

  328. 	ANDQ	AX, CX

  329. 	XORQ	BX, CX

  330. 	MOVQ	CX, (9*8)(REG_P3)

  331. 

  332. 	MOVQ	(10*8)(REG_P1), BX

  333. 	MOVQ 	(10*8)(REG_P2), CX

  334. 	XORQ	BX, CX

  335. 	ANDQ	AX, CX

  336. 	XORQ	BX, CX

  337. 	MOVQ	CX, (10*8)(REG_P3)

  338. 

  339. 	MOVQ	(11*8)(REG_P1), BX

  340. 	MOVQ 	(11*8)(REG_P2), CX

  341. 	XORQ	BX, CX

  342. 	ANDQ	AX, CX

  343. 	XORQ	BX, CX

  344. 	MOVQ	CX, (11*8)(REG_P3)

  345. 

  346. 	RET

  347. 

  348. TEXT ·fp751AddReduced(SB), NOSPLIT, $0-24

  349. 

  350. 	MOVQ	z+0(FP), REG_P3

  351. 	MOVQ	x+8(FP), REG_P1

  352. 	MOVQ	y+16(FP), REG_P2

  353. 

  354. 	MOVQ	(REG_P1), R8

  355. 	MOVQ	(8)(REG_P1), R9

  356. 	MOVQ	(16)(REG_P1), R10

  357. 	MOVQ	(24)(REG_P1), R11

  358. 	MOVQ	(32)(REG_P1), R12

  359. 	MOVQ	(40)(REG_P1), R13

  360. 	MOVQ	(48)(REG_P1), R14

  361. 	MOVQ	(56)(REG_P1), R15

  362. 	MOVQ	(64)(REG_P1), CX

  363. 	ADDQ	(REG_P2), R8

  364. 	ADCQ	(8)(REG_P2), R9

  365. 	ADCQ	(16)(REG_P2), R10

  366. 	ADCQ	(24)(REG_P2), R11

  367. 	ADCQ	(32)(REG_P2), R12

  368. 	ADCQ	(40)(REG_P2), R13

  369. 	ADCQ	(48)(REG_P2), R14

  370. 	ADCQ	(56)(REG_P2), R15

  371. 	ADCQ	(64)(REG_P2), CX

  372. 	MOVQ	(72)(REG_P1), AX

  373. 	ADCQ	(72)(REG_P2), AX

  374. 	MOVQ	AX, (72)(REG_P3)

  375. 	MOVQ	(80)(REG_P1), AX

  376. 	ADCQ	(80)(REG_P2), AX

  377. 	MOVQ	AX, (80)(REG_P3)

  378. 	MOVQ	(88)(REG_P1), AX

  379. 	ADCQ	(88)(REG_P2), AX

  380. 	MOVQ	AX, (88)(REG_P3)

  381. 

  382. 	MOVQ	P751X2_0, AX

  383. 	SUBQ	AX, R8

  384. 	MOVQ	P751X2_1, AX

  385. 	SBBQ	AX, R9

  386. 	SBBQ	AX, R10

  387. 	SBBQ	AX, R11

  388. 	SBBQ	AX, R12

  389. 	MOVQ	P751X2_5, AX

  390. 	SBBQ	AX, R13

  391. 	MOVQ	P751X2_6, AX

  392. 	SBBQ	AX, R14

  393. 	MOVQ	P751X2_7, AX

  394. 	SBBQ	AX, R15

  395. 	MOVQ	P751X2_8, AX

  396. 	SBBQ	AX, CX

  397. 	MOVQ	R8, (REG_P3)

  398. 	MOVQ	R9, (8)(REG_P3)

  399. 	MOVQ	R10, (16)(REG_P3)

  400. 	MOVQ	R11, (24)(REG_P3)

  401. 	MOVQ	R12, (32)(REG_P3)

  402. 	MOVQ	R13, (40)(REG_P3)

  403. 	MOVQ	R14, (48)(REG_P3)

  404. 	MOVQ	R15, (56)(REG_P3)

  405. 	MOVQ	CX, (64)(REG_P3)

  406. 	MOVQ	(72)(REG_P3), R8

  407. 	MOVQ	(80)(REG_P3), R9

  408. 	MOVQ	(88)(REG_P3), R10

  409. 	MOVQ	P751X2_9, AX

  410. 	SBBQ	AX, R8

  411. 	MOVQ	P751X2_10, AX

  412. 	SBBQ	AX, R9

  413. 	MOVQ	P751X2_11, AX

  414. 	SBBQ	AX, R10

  415. 	MOVQ	R8, (72)(REG_P3)

  416. 	MOVQ	R9, (80)(REG_P3)

  417. 	MOVQ	R10, (88)(REG_P3)

  418. 	ZERO_AX_WITHOUT_CLOBBERING_FLAGS

  419. 	SBBQ	$0, AX

  420. 

  421. 	MOVQ	P751X2_0, SI

  422. 	ANDQ	AX, SI

  423. 	MOVQ	P751X2_1, R8

  424. 	ANDQ	AX, R8

  425. 	MOVQ	P751X2_5, R9

  426. 	ANDQ	AX, R9

  427. 	MOVQ	P751X2_6, R10

  428. 	ANDQ	AX, R10

  429. 	MOVQ	P751X2_7, R11

  430. 	ANDQ	AX, R11

  431. 	MOVQ	P751X2_8, R12

  432. 	ANDQ	AX, R12

  433. 	MOVQ	P751X2_9, R13

  434. 	ANDQ	AX, R13

  435. 	MOVQ	P751X2_10, R14

  436. 	ANDQ	AX, R14

  437. 	MOVQ	P751X2_11, R15

  438. 	ANDQ	AX, R15

  439. 

  440. 	MOVQ	(REG_P3), AX

  441. 	ADDQ	SI, AX

  442. 	MOVQ	AX, (REG_P3)

  443. 	MOVQ	(8)(REG_P3), AX

  444. 	ADCQ	R8, AX

  445. 	MOVQ	AX, (8)(REG_P3)

  446. 	MOVQ	(16)(REG_P3), AX

  447. 	ADCQ	R8, AX

  448. 	MOVQ	AX, (16)(REG_P3)

  449. 	MOVQ	(24)(REG_P3), AX

  450. 	ADCQ	R8, AX

  451. 	MOVQ	AX, (24)(REG_P3)

  452. 	MOVQ	(32)(REG_P3), AX

  453. 	ADCQ	R8, AX

  454. 	MOVQ	AX, (32)(REG_P3)

  455. 	MOVQ	(40)(REG_P3), AX

  456. 	ADCQ	R9, AX

  457. 	MOVQ	AX, (40)(REG_P3)

  458. 	MOVQ	(48)(REG_P3), AX

  459. 	ADCQ	R10, AX

  460. 	MOVQ	AX, (48)(REG_P3)

  461. 	MOVQ	(56)(REG_P3), AX

  462. 	ADCQ	R11, AX

  463. 	MOVQ	AX, (56)(REG_P3)

  464. 	MOVQ	(64)(REG_P3), AX

  465. 	ADCQ	R12, AX

  466. 	MOVQ	AX, (64)(REG_P3)

  467. 	MOVQ	(72)(REG_P3), AX

  468. 	ADCQ	R13, AX

  469. 	MOVQ	AX, (72)(REG_P3)

  470. 	MOVQ	(80)(REG_P3), AX

  471. 	ADCQ	R14, AX

  472. 	MOVQ	AX, (80)(REG_P3)

  473. 	MOVQ	(88)(REG_P3), AX

  474. 	ADCQ	R15, AX

  475. 	MOVQ	AX, (88)(REG_P3)

  476. 

  477. 	RET

  478. 

  479. TEXT ·fp751SubReduced(SB), NOSPLIT, $0-24

  480. 

  481. 	MOVQ	z+0(FP),  REG_P3

  482. 	MOVQ	x+8(FP),  REG_P1

  483. 	MOVQ	y+16(FP),  REG_P2

  484. 

  485. 	MOVQ	(REG_P1), R8

  486. 	MOVQ	(8)(REG_P1), R9

  487. 	MOVQ	(16)(REG_P1), R10

  488. 	MOVQ	(24)(REG_P1), R11

  489. 	MOVQ	(32)(REG_P1), R12

  490. 	MOVQ	(40)(REG_P1), R13

  491. 	MOVQ	(48)(REG_P1), R14

  492. 	MOVQ	(56)(REG_P1), R15

  493. 	MOVQ	(64)(REG_P1), CX

  494. 	SUBQ	(REG_P2), R8

  495. 	SBBQ	(8)(REG_P2), R9

  496. 	SBBQ	(16)(REG_P2), R10

  497. 	SBBQ	(24)(REG_P2), R11

  498. 	SBBQ	(32)(REG_P2), R12

  499. 	SBBQ	(40)(REG_P2), R13

  500. 	SBBQ	(48)(REG_P2), R14

  501. 	SBBQ	(56)(REG_P2), R15

  502. 	SBBQ	(64)(REG_P2), CX

  503. 	MOVQ	R8, (REG_P3)

  504. 	MOVQ	R9, (8)(REG_P3)

  505. 	MOVQ	R10, (16)(REG_P3)

  506. 	MOVQ	R11, (24)(REG_P3)

  507. 	MOVQ	R12, (32)(REG_P3)

  508. 	MOVQ	R13, (40)(REG_P3)

  509. 	MOVQ	R14, (48)(REG_P3)

  510. 	MOVQ	R15, (56)(REG_P3)

  511. 	MOVQ	CX, (64)(REG_P3)

  512. 	MOVQ	(72)(REG_P1), AX

  513. 	SBBQ	(72)(REG_P2), AX

  514. 	MOVQ	AX, (72)(REG_P3)

  515. 	MOVQ	(80)(REG_P1), AX

  516. 	SBBQ	(80)(REG_P2), AX

  517. 	MOVQ	AX, (80)(REG_P3)

  518. 	MOVQ	(88)(REG_P1), AX

  519. 	SBBQ	(88)(REG_P2), AX

  520. 	MOVQ	AX, (88)(REG_P3)

  521. 	ZERO_AX_WITHOUT_CLOBBERING_FLAGS

  522. 	SBBQ	$0, AX

  523. 

  524. 	MOVQ	P751X2_0, SI

  525. 	ANDQ	AX, SI

  526. 	MOVQ	P751X2_1, R8

  527. 	ANDQ	AX, R8

  528. 	MOVQ	P751X2_5, R9

  529. 	ANDQ	AX, R9

  530. 	MOVQ	P751X2_6, R10

  531. 	ANDQ	AX, R10

  532. 	MOVQ	P751X2_7, R11

  533. 	ANDQ	AX, R11

  534. 	MOVQ	P751X2_8, R12

  535. 	ANDQ	AX, R12

  536. 	MOVQ	P751X2_9, R13

  537. 	ANDQ	AX, R13

  538. 	MOVQ	P751X2_10, R14

  539. 	ANDQ	AX, R14

  540. 	MOVQ	P751X2_11, R15

  541. 	ANDQ	AX, R15

  542. 

  543. 	MOVQ	(REG_P3), AX

  544. 	ADDQ	SI, AX

  545. 	MOVQ	AX, (REG_P3)

  546. 	MOVQ	(8)(REG_P3), AX

  547. 	ADCQ	R8, AX

  548. 	MOVQ	AX, (8)(REG_P3)

  549. 	MOVQ	(16)(REG_P3), AX

  550. 	ADCQ	R8, AX

  551. 	MOVQ	AX, (16)(REG_P3)

  552. 	MOVQ	(24)(REG_P3), AX

  553. 	ADCQ	R8, AX

  554. 	MOVQ	AX, (24)(REG_P3)

  555. 	MOVQ	(32)(REG_P3), AX

  556. 	ADCQ	R8, AX

  557. 	MOVQ	AX, (32)(REG_P3)

  558. 	MOVQ	(40)(REG_P3), AX

  559. 	ADCQ	R9, AX

  560. 	MOVQ	AX, (40)(REG_P3)

  561. 	MOVQ	(48)(REG_P3), AX

  562. 	ADCQ	R10, AX

  563. 	MOVQ	AX, (48)(REG_P3)

  564. 	MOVQ	(56)(REG_P3), AX

  565. 	ADCQ	R11, AX

  566. 	MOVQ	AX, (56)(REG_P3)

  567. 	MOVQ	(64)(REG_P3), AX

  568. 	ADCQ	R12, AX

  569. 	MOVQ	AX, (64)(REG_P3)

  570. 	MOVQ	(72)(REG_P3), AX

  571. 	ADCQ	R13, AX

  572. 	MOVQ	AX, (72)(REG_P3)

  573. 	MOVQ	(80)(REG_P3), AX

  574. 	ADCQ	R14, AX

  575. 	MOVQ	AX, (80)(REG_P3)

  576. 	MOVQ	(88)(REG_P3), AX

  577. 	ADCQ	R15, AX

  578. 	MOVQ	AX, (88)(REG_P3)

  579. 

  580. 	RET

  581. 

  582. TEXT ·fp751Mul(SB), $96-24

  583. 

  584. 	// Here we store the destination in CX instead of in REG_P3 because the

  585. 	// multiplication instructions use DX as an implicit destination

  586. 	// operand: MULQ $REG sets DX:AX <-- AX * $REG.

  587. 

  588. 	MOVQ	z+0(FP), CX

  589. 	MOVQ	x+8(FP), REG_P1

  590. 	MOVQ	y+16(FP), REG_P2

  591. 

  592. 	XORQ	AX, AX

  593. 	MOVQ	(48)(REG_P1), R8

  594. 	MOVQ	(56)(REG_P1), R9

  595. 	MOVQ	(64)(REG_P1), R10

  596. 	MOVQ	(72)(REG_P1), R11

  597. 	MOVQ	(80)(REG_P1), R12

  598. 	MOVQ	(88)(REG_P1), R13

  599. 	ADDQ	(REG_P1), R8

  600. 	ADCQ	(8)(REG_P1), R9

  601. 	ADCQ	(16)(REG_P1), R10

  602. 	ADCQ	(24)(REG_P1), R11

  603. 	ADCQ	(32)(REG_P1), R12

  604. 	ADCQ	(40)(REG_P1), R13

  605. 	MOVQ	R8, (CX)

  606. 	MOVQ	R9, (8)(CX)

  607. 	MOVQ	R10, (16)(CX)

  608. 	MOVQ	R11, (24)(CX)

  609. 	MOVQ	R12, (32)(CX)

  610. 	MOVQ	R13, (40)(CX)

  611. 	SBBQ	$0, AX

  612. 

  613. 	XORQ	DX, DX

  614. 	MOVQ	(48)(REG_P2), R8

  615. 	MOVQ	(56)(REG_P2), R9

  616. 	MOVQ	(64)(REG_P2), R10

  617. 	MOVQ	(72)(REG_P2), R11

  618. 	MOVQ	(80)(REG_P2), R12

  619. 	MOVQ	(88)(REG_P2), R13

  620. 	ADDQ	(REG_P2), R8

  621. 	ADCQ	(8)(REG_P2), R9

  622. 	ADCQ	(16)(REG_P2), R10

  623. 	ADCQ	(24)(REG_P2), R11

  624. 	ADCQ	(32)(REG_P2), R12

  625. 	ADCQ	(40)(REG_P2), R13

  626. 	MOVQ	R8, (48)(CX)

  627. 	MOVQ	R9, (56)(CX)

  628. 	MOVQ	R10, (64)(CX)

  629. 	MOVQ	R11, (72)(CX)

  630. 	MOVQ	R12, (80)(CX)

  631. 	MOVQ	R13, (88)(CX)

  632. 	SBBQ	$0, DX

  633. 	MOVQ	AX, (80)(SP)

  634. 	MOVQ	DX, (88)(SP)

  635. 

  636. 	// (SP[0-8],R10,R8,R9) <- (AH+AL)*(BH+BL)

  637. 

  638. 	MOVQ	(CX), R11

  639. 	MOVQ	R8, AX

  640. 	MULQ	R11

  641. 	MOVQ	AX, (SP)		// c0

  642. 	MOVQ	DX, R14

  643. 

  644. 	XORQ	R15, R15

  645. 	MOVQ	R9, AX

  646. 	MULQ	R11

  647. 	XORQ	R9, R9

  648. 	ADDQ	AX, R14

  649. 	ADCQ	DX, R9

  650. 

  651. 	MOVQ	(8)(CX), R12

  652. 	MOVQ	R8, AX

  653. 	MULQ	R12

  654. 	ADDQ	AX, R14

  655. 	MOVQ	R14, (8)(SP)		// c1

  656. 	ADCQ	DX, R9

  657. 	ADCQ	$0, R15

  658. 

  659. 	XORQ	R8, R8

  660. 	MOVQ	R10, AX

  661. 	MULQ	R11

  662. 	ADDQ	AX, R9

  663. 	MOVQ	(48)(CX), R13

  664. 	ADCQ	DX, R15

  665. 	ADCQ	$0, R8

  666. 

  667. 	MOVQ	(16)(CX), AX

  668. 	MULQ	R13

  669. 	ADDQ	AX, R9

  670. 	ADCQ	DX, R15

  671. 	MOVQ	(56)(CX), AX

  672. 	ADCQ	$0, R8

  673. 

  674. 	MULQ	R12

  675. 	ADDQ	AX, R9

  676. 	MOVQ	R9, (16)(SP)		// c2

  677. 	ADCQ	DX, R15

  678. 	ADCQ	$0, R8

  679. 

  680. 	XORQ	R9, R9

  681. 	MOVQ	(72)(CX), AX

  682. 	MULQ	R11

  683. 	ADDQ	AX, R15

  684. 	ADCQ	DX, R8

  685. 	ADCQ	$0, R9

  686. 

  687. 	MOVQ	(24)(CX), AX

  688. 	MULQ	R13

  689. 	ADDQ	AX, R15

  690. 	ADCQ	DX, R8

  691. 	ADCQ	$0, R9

  692. 

  693. 	MOVQ	R10, AX

  694. 	MULQ	R12

  695. 	ADDQ	AX, R15

  696. 	ADCQ	DX, R8

  697. 	ADCQ	$0, R9

  698. 

  699. 	MOVQ	(16)(CX), R14

  700. 	MOVQ	(56)(CX), AX

  701. 	MULQ	R14

  702. 	ADDQ	AX, R15

  703. 	MOVQ	R15, (24)(SP)		// c3

  704. 	ADCQ	DX, R8

  705. 	ADCQ	$0, R9

  706. 

  707. 	XORQ	R10, R10

  708. 	MOVQ	(80)(CX), AX

  709. 	MULQ	R11

  710. 	ADDQ	AX, R8

  711. 	ADCQ	DX, R9

  712. 	ADCQ	$0, R10

  713. 

  714. 	MOVQ	(64)(CX), AX

  715. 	MULQ	R14

  716. 	ADDQ	AX, R8

  717. 	ADCQ	DX, R9

  718. 	ADCQ	$0, R10

  719. 

  720. 	MOVQ	(48)(CX), R15

  721. 	MOVQ	(32)(CX), AX

  722. 	MULQ	R15

  723. 	ADDQ	AX, R8

  724. 	ADCQ	DX, R9

  725. 	ADCQ	$0, R10

  726. 

  727. 	MOVQ	(72)(CX), AX

  728. 	MULQ	R12

  729. 	ADDQ	AX, R8

  730. 	ADCQ	DX, R9

  731. 	ADCQ	$0, R10

  732. 

  733. 	MOVQ	(24)(CX), R13

  734. 	MOVQ	(56)(CX), AX

  735. 	MULQ	R13

  736. 	ADDQ	AX, R8

  737. 	MOVQ	R8, (32)(SP)		// c4

  738. 	ADCQ	DX, R9

  739. 	ADCQ	$0, R10

  740. 

  741. 	XORQ	R8, R8

  742. 	MOVQ	(88)(CX), AX

  743. 	MULQ	R11

  744. 	ADDQ	AX, R9

  745. 	ADCQ	DX, R10

  746. 	ADCQ	$0, R8

  747. 

  748. 	MOVQ	(64)(CX), AX

  749. 	MULQ	R13

  750. 	ADDQ	AX, R9

  751. 	ADCQ	DX, R10

  752. 	ADCQ	$0, R8

  753. 

  754. 	MOVQ	(72)(CX), AX

  755. 	MULQ	R14

  756. 	ADDQ	AX, R9

  757. 	ADCQ	DX, R10

  758. 	ADCQ	$0, R8

  759. 

  760. 	MOVQ	(40)(CX), AX

  761. 	MULQ	R15

  762. 	ADDQ	AX, R9

  763. 	ADCQ	DX, R10

  764. 	ADCQ	$0, R8

  765. 

  766. 	MOVQ	(80)(CX), AX

  767. 	MULQ	R12

  768. 	ADDQ	AX, R9

  769. 	ADCQ	DX, R10

  770. 	ADCQ	$0, R8

  771. 

  772. 	MOVQ	(32)(CX), R15

  773. 	MOVQ	(56)(CX), AX

  774. 	MULQ	R15

  775. 	ADDQ	AX, R9

  776. 	MOVQ	R9, (40)(SP)		// c5

  777. 	ADCQ	DX, R10

  778. 	ADCQ	$0, R8

  779. 

  780. 	XORQ	R9, R9

  781. 	MOVQ	(64)(CX), AX

  782. 	MULQ	R15

  783. 	ADDQ	AX, R10

  784. 	ADCQ	DX, R8

  785. 	ADCQ	$0, R9

  786. 

  787. 	MOVQ	(88)(CX), AX

  788. 	MULQ	R12

  789. 	ADDQ	AX, R10

  790. 	ADCQ	DX, R8

  791. 	ADCQ	$0, R9

  792. 

  793. 	MOVQ	(80)(CX), AX

  794. 	MULQ	R14

  795. 	ADDQ	AX, R10

  796. 	ADCQ	DX, R8

  797. 	ADCQ	$0, R9

  798. 

  799. 	MOVQ	(40)(CX), R11

  800. 	MOVQ	(56)(CX), AX

  801. 	MULQ	R11

  802. 	ADDQ	AX, R10

  803. 	ADCQ	DX, R8

  804. 	ADCQ	$0, R9

  805. 

  806. 	MOVQ	(72)(CX), AX

  807. 	MULQ	R13

  808. 	ADDQ	AX, R10

  809. 	MOVQ	R10, (48)(SP)		// c6

  810. 	ADCQ	DX, R8

  811. 	ADCQ	$0, R9

  812. 

  813. 	XORQ	R10, R10

  814. 	MOVQ	(88)(CX), AX

  815. 	MULQ	R14

  816. 	ADDQ	AX, R8

  817. 	ADCQ	DX, R9

  818. 	ADCQ	$0, R10

  819. 

  820. 	MOVQ	(64)(CX), AX

  821. 	MULQ	R11

  822. 	ADDQ	AX, R8

  823. 	ADCQ	DX, R9

  824. 	ADCQ	$0, R10

  825. 

  826. 	MOVQ	(80)(CX), AX

  827. 	MULQ	R13

  828. 	ADDQ	AX, R8

  829. 	ADCQ	DX, R9

  830. 	ADCQ	$0, R10

  831. 

  832. 	MOVQ	(72)(CX), AX

  833. 	MULQ	R15

  834. 	ADDQ	AX, R8

  835. 	MOVQ	R8, (56)(SP)		// c7

  836. 	ADCQ	DX, R9

  837. 	ADCQ	$0, R10

  838. 

  839. 	XORQ	R8, R8

  840. 	MOVQ	(72)(CX), AX

  841. 	MULQ	R11

  842. 	ADDQ	AX, R9

  843. 	ADCQ	DX, R10

  844. 	ADCQ	$0, R8

  845. 

  846. 	MOVQ	(80)(CX), AX

  847. 	MULQ	R15

  848. 	ADDQ	AX, R9

  849. 	ADCQ	DX, R10

  850. 	ADCQ	$0, R8

  851. 

  852. 	MOVQ	(88)(CX), AX

  853. 	MULQ	R13

  854. 	ADDQ	AX, R9

  855. 	MOVQ	R9, (64)(SP)		// c8

  856. 	ADCQ	DX, R10

  857. 	ADCQ	$0, R8

  858. 

  859. 	XORQ	R9, R9

  860. 	MOVQ	(88)(CX), AX

  861. 	MULQ	R15

  862. 	ADDQ	AX, R10

  863. 	ADCQ	DX, R8

  864. 	ADCQ	$0, R9

  865. 

  866. 	MOVQ	(80)(CX), AX

  867. 	MULQ	R11

  868. 	ADDQ	AX, R10			// c9

  869. 	ADCQ	DX, R8

  870. 	ADCQ	$0, R9

  871. 

  872. 	MOVQ	(88)(CX), AX

  873. 	MULQ	R11

  874. 	ADDQ	AX, R8			// c10

  875. 	ADCQ	DX, R9			// c11

  876. 

  877. 	MOVQ	(88)(SP), AX

  878. 	MOVQ	(CX), DX

  879. 	ANDQ	AX, R12

  880. 	ANDQ	AX, R14

  881. 	ANDQ	AX, DX

  882. 	ANDQ	AX, R13

  883. 	ANDQ	AX, R15

  884. 	ANDQ	AX, R11

  885. 	MOVQ	(48)(SP), AX

  886. 	ADDQ	AX, DX

  887. 	MOVQ	(56)(SP), AX

  888. 	ADCQ	AX, R12

  889. 	MOVQ	(64)(SP), AX

  890. 	ADCQ	AX, R14

  891. 	ADCQ	R10, R13

  892. 	ADCQ	R8, R15

  893. 	ADCQ	R9, R11

  894. 	MOVQ	(80)(SP), AX

  895. 	MOVQ	DX, (48)(SP)

  896. 	MOVQ	R12, (56)(SP)

  897. 	MOVQ	R14, (64)(SP)

  898. 	MOVQ	R13, (72)(SP)

  899. 	MOVQ	R15, (80)(SP)

  900. 	MOVQ	R11, (88)(SP)

  901. 

  902. 	MOVQ	(48)(CX), R8

  903. 	MOVQ	(56)(CX), R9

  904. 	MOVQ	(64)(CX), R10

  905. 	MOVQ	(72)(CX), R11

  906. 	MOVQ	(80)(CX), R12

  907. 	MOVQ	(88)(CX), R13

  908. 	ANDQ	AX, R8

  909. 	ANDQ	AX, R9

  910. 	ANDQ	AX, R10

  911. 	ANDQ	AX, R11

  912. 	ANDQ	AX, R12

  913. 	ANDQ	AX, R13

  914. 	MOVQ	(48)(SP), AX

  915. 	ADDQ	AX, R8

  916. 	MOVQ	(56)(SP), AX

  917. 	ADCQ	AX, R9

  918. 	MOVQ	(64)(SP), AX

  919. 	ADCQ	AX, R10

  920. 	MOVQ	(72)(SP), AX

  921. 	ADCQ	AX, R11

  922. 	MOVQ	(80)(SP), AX

  923. 	ADCQ	AX, R12

  924. 	MOVQ	(88)(SP), AX

  925. 	ADCQ	AX, R13

  926. 	MOVQ	R8, (48)(SP)

  927. 	MOVQ	R9, (56)(SP)

  928. 	MOVQ	R11, (72)(SP)

  929. 

  930. 	// CX[0-11] <- AL*BL

  931. 	MOVQ	(REG_P1), R11

  932. 	MOVQ	(REG_P2), AX

  933. 	MULQ	R11

  934. 	XORQ	R9, R9

  935. 	MOVQ	AX, (CX)		// c0

  936. 	MOVQ	R10, (64)(SP)

  937. 	MOVQ	DX, R8

  938. 

  939. 	MOVQ	(8)(REG_P2), AX

  940. 	MULQ	R11

  941. 	XORQ	R10, R10

  942. 	ADDQ	AX, R8

  943. 	MOVQ	R12, (80)(SP)

  944. 	ADCQ	DX, R9

  945. 

  946. 	MOVQ	(8)(REG_P1), R12

  947. 	MOVQ	(REG_P2), AX

  948. 	MULQ	R12

  949. 	ADDQ	AX, R8

  950. 	MOVQ	R8, (8)(CX)		// c1

  951. 	ADCQ	DX, R9

  952. 	MOVQ	R13, (88)(SP)

  953. 	ADCQ	$0, R10

  954. 

  955. 	XORQ	R8, R8

  956. 	MOVQ	(16)(REG_P2), AX

  957. 	MULQ	R11

  958. 	ADDQ	AX, R9

  959. 	ADCQ	DX, R10

  960. 	ADCQ	$0, R8

  961. 

  962. 	MOVQ	(REG_P2), R13

  963. 	MOVQ	(16)(REG_P1), AX

  964. 	MULQ	R13

  965. 	ADDQ	AX, R9

  966. 	ADCQ	DX, R10

  967. 	ADCQ	$0, R8

  968. 

  969. 	MOVQ	(8)(REG_P2), AX

  970. 	MULQ	R12

  971. 	ADDQ	AX, R9

  972. 	MOVQ	R9, (16)(CX)		// c2

  973. 	ADCQ	DX, R10

  974. 	ADCQ	$0, R8

  975. 

  976. 	XORQ	R9, R9

  977. 	MOVQ	(24)(REG_P2), AX

  978. 	MULQ	R11

  979. 	ADDQ	AX, R10

  980. 	ADCQ	DX, R8

  981. 	ADCQ	$0, R9

  982. 

  983. 	MOVQ	(24)(REG_P1), AX

  984. 	MULQ	R13

  985. 	ADDQ	AX, R10

  986. 	ADCQ	DX, R8

  987. 	ADCQ	$0, R9

  988. 

  989. 	MOVQ	(16)(REG_P2), AX

  990. 	MULQ	R12

  991. 	ADDQ	AX, R10

  992. 	ADCQ	DX, R8

  993. 	ADCQ	$0, R9

  994. 

  995. 	MOVQ	(16)(REG_P1), R14

  996. 	MOVQ	(8)(REG_P2), AX

  997. 	MULQ	R14

  998. 	ADDQ	AX, R10

  999. 	MOVQ	R10, (24)(CX)		// c3

  1000. 	ADCQ	DX, R8

  1001. 	ADCQ	$0, R9

  1002. 

  1003. 	XORQ	R10, R10

  1004. 	MOVQ	(32)(REG_P2), AX

  1005. 	MULQ	R11

  1006. 	ADDQ	AX, R8

  1007. 	ADCQ	DX, R9

  1008. 	ADCQ	$0, R10

  1009. 

  1010. 	MOVQ	(16)(REG_P2), AX

  1011. 	MULQ	R14

  1012. 	ADDQ	AX, R8

  1013. 	ADCQ	DX, R9

  1014. 	ADCQ	$0, R10

  1015. 

  1016. 	MOVQ	(32)(REG_P1), AX

  1017. 	MULQ	R13

  1018. 	ADDQ	AX, R8

  1019. 	ADCQ	DX, R9

  1020. 	ADCQ	$0, R10

  1021. 

  1022. 	MOVQ	(24)(REG_P2), AX

  1023. 	MULQ	R12

  1024. 	ADDQ	AX, R8

  1025. 	ADCQ	DX, R9

  1026. 	ADCQ	$0, R10

  1027. 

  1028. 	MOVQ	(24)(REG_P1), R13

  1029. 	MOVQ	(8)(REG_P2), AX

  1030. 	MULQ	R13

  1031. 	ADDQ	AX, R8

  1032. 	MOVQ	R8, (32)(CX)		// c4

  1033. 	ADCQ	DX, R9

  1034. 	ADCQ	$0, R10

  1035. 

  1036. 	XORQ	R8, R8

  1037. 	MOVQ	(40)(REG_P2), AX

  1038. 	MULQ	R11

  1039. 	ADDQ	AX, R9

  1040. 	ADCQ	DX, R10

  1041. 	ADCQ	$0, R8

  1042. 

  1043. 	MOVQ	(16)(REG_P2), AX

  1044. 	MULQ	R13

  1045. 	ADDQ	AX, R9

  1046. 	ADCQ	DX, R10

  1047. 	ADCQ	$0, R8

  1048. 

  1049. 	MOVQ	(24)(REG_P2), AX

  1050. 	MULQ	R14

  1051. 	ADDQ	AX, R9

  1052. 	ADCQ	DX, R10

  1053. 	ADCQ	$0, R8

  1054. 

  1055. 	MOVQ	(40)(REG_P1), R11

  1056. 	MOVQ	(REG_P2), AX

  1057. 	MULQ	R11

  1058. 	ADDQ	AX, R9

  1059. 	ADCQ	DX, R10

  1060. 	ADCQ	$0, R8

  1061. 

  1062. 	MOVQ	(32)(REG_P2), AX

  1063. 	MULQ	R12

  1064. 	ADDQ	AX, R9

  1065. 	ADCQ	DX, R10

  1066. 	ADCQ	$0, R8

  1067. 

  1068. 	MOVQ	(32)(REG_P1), R15

  1069. 	MOVQ	(8)(REG_P2), AX

  1070. 	MULQ	R15

  1071. 	ADDQ	AX, R9

  1072. 	MOVQ	R9, (40)(CX)		//c5

  1073. 	ADCQ	DX, R10

  1074. 	ADCQ	$0, R8

  1075. 

  1076. 	XORQ	R9, R9

  1077. 	MOVQ	(16)(REG_P2), AX

  1078. 	MULQ	R15

  1079. 	ADDQ	AX, R10

  1080. 	ADCQ	DX, R8

  1081. 	ADCQ	$0, R9

  1082. 

  1083. 	MOVQ	(40)(REG_P2), AX

  1084. 	MULQ	R12

  1085. 	ADDQ	AX, R10

  1086. 	ADCQ	DX, R8

  1087. 	ADCQ	$0, R9

  1088. 

  1089. 	MOVQ	(32)(REG_P2), AX

  1090. 	MULQ	R14

  1091. 	ADDQ	AX, R10

  1092. 	ADCQ	DX, R8

  1093. 	ADCQ	$0, R9

  1094. 

  1095. 	MOVQ	(8)(REG_P2), AX

  1096. 	MULQ	R11

  1097. 	ADDQ	AX, R10

  1098. 	ADCQ	DX, R8

  1099. 	ADCQ	$0, R9

  1100. 

  1101. 	MOVQ	(24)(REG_P2), AX

  1102. 	MULQ	R13

  1103. 	ADDQ	AX, R10

  1104. 	MOVQ	R10, (48)(CX)		// c6

  1105. 	ADCQ	DX, R8

  1106. 	ADCQ	$0, R9

  1107. 

  1108. 	XORQ	R10, R10

  1109. 	MOVQ	(40)(REG_P2), AX

  1110. 	MULQ	R14

  1111. 	ADDQ	AX, R8

  1112. 	ADCQ	DX, R9

  1113. 	ADCQ	$0, R10

  1114. 

  1115. 	MOVQ	(16)(REG_P2), AX

  1116. 	MULQ	R11

  1117. 	ADDQ	AX, R8

  1118. 	ADCQ	DX, R9

  1119. 	ADCQ	$0, R10

  1120. 

  1121. 	MOVQ	(32)(REG_P2), AX

  1122. 	MULQ	R13

  1123. 	ADDQ	AX, R8

  1124. 	ADCQ	DX, R9

  1125. 	ADCQ	$0, R10

  1126. 

  1127. 	MOVQ	(24)(REG_P2), AX

  1128. 	MULQ	R15

  1129. 	ADDQ	AX, R8

  1130. 	MOVQ	R8, (56)(CX)		// c7

  1131. 	ADCQ	DX, R9

  1132. 	ADCQ	$0, R10

  1133. 

  1134. 	XORQ	R8, R8

  1135. 	MOVQ	(24)(REG_P2), AX

  1136. 	MULQ	R11

  1137. 	ADDQ	AX, R9

  1138. 	ADCQ	DX, R10

  1139. 	ADCQ	$0, R8

  1140. 

  1141. 	MOVQ	(32)(REG_P2), AX

  1142. 	MULQ	R15

  1143. 	ADDQ	AX, R9

  1144. 	ADCQ	DX, R10

  1145. 	ADCQ	$0, R8

  1146. 

  1147. 	MOVQ	(40)(REG_P2), AX

  1148. 	MULQ	R13

  1149. 	ADDQ	AX, R9

  1150. 	MOVQ	R9, (64)(CX)		// c8

  1151. 	ADCQ	DX, R10

  1152. 	ADCQ	$0, R8

  1153. 

  1154. 	XORQ	R9, R9

  1155. 	MOVQ	(40)(REG_P2), AX

  1156. 	MULQ	R15

  1157. 	ADDQ	AX, R10

  1158. 	ADCQ	DX, R8

  1159. 	ADCQ	$0, R9

  1160. 

  1161. 	MOVQ	(32)(REG_P2), AX

  1162. 	MULQ	R11

  1163. 	ADDQ	AX, R10

  1164. 	MOVQ	R10, (72)(CX)		// c9

  1165. 	ADCQ	DX, R8

  1166. 	ADCQ	$0, R9

  1167. 

  1168. 	MOVQ	(40)(REG_P2), AX

  1169. 	MULQ	R11

  1170. 	ADDQ	AX, R8

  1171. 	MOVQ	R8, (80)(CX)		// c10

  1172. 	ADCQ	DX, R9

  1173. 	MOVQ	R9, (88)(CX)		// c11

  1174. 

  1175. 	// CX[12-23] <- AH*BH

  1176. 	MOVQ	(48)(REG_P1), R11

  1177. 	MOVQ	(48)(REG_P2), AX

  1178. 	MULQ	R11

  1179. 	XORQ	R9, R9

  1180. 	MOVQ	AX, (96)(CX)		// c0

  1181. 	MOVQ	DX, R8

  1182. 

  1183. 	MOVQ	(56)(REG_P2), AX

  1184. 	MULQ	R11

  1185. 	XORQ	R10, R10

  1186. 	ADDQ	AX, R8

  1187. 	ADCQ	DX, R9

  1188. 

  1189. 	MOVQ	(56)(REG_P1), R12

  1190. 	MOVQ	(48)(REG_P2), AX

  1191. 	MULQ	R12

  1192. 	ADDQ	AX, R8

  1193. 	MOVQ	R8, (104)(CX)		// c1

  1194. 	ADCQ	DX, R9

  1195. 	ADCQ	$0, R10

  1196. 

  1197. 	XORQ	R8, R8

  1198. 	MOVQ	(64)(REG_P2), AX

  1199. 	MULQ	R11

  1200. 	ADDQ	AX, R9

  1201. 	ADCQ	DX, R10

  1202. 	ADCQ	$0, R8

  1203. 

  1204. 	MOVQ	(48)(REG_P2), R13

  1205. 	MOVQ	(64)(REG_P1), AX

  1206. 	MULQ	R13

  1207. 	ADDQ	AX, R9

  1208. 	ADCQ	DX, R10

  1209. 	ADCQ	$0, R8

  1210. 

  1211. 	MOVQ	(56)(REG_P2), AX

  1212. 	MULQ	R12

  1213. 	ADDQ	AX, R9

  1214. 	MOVQ	R9, (112)(CX)		// c2

  1215. 	ADCQ	DX, R10

  1216. 	ADCQ	$0, R8

  1217. 

  1218. 	XORQ	R9, R9

  1219. 	MOVQ	(72)(REG_P2), AX

  1220. 	MULQ	R11

  1221. 	ADDQ	AX, R10

  1222. 	ADCQ	DX, R8

  1223. 	ADCQ	$0, R9

  1224. 

  1225. 	MOVQ	(72)(REG_P1), AX

  1226. 	MULQ	R13

  1227. 	ADDQ	AX, R10

  1228. 	ADCQ	DX, R8

  1229. 	ADCQ	$0, R9

  1230. 

  1231. 	MOVQ	(64)(REG_P2), AX

  1232. 	MULQ	R12

  1233. 	ADDQ	AX, R10

  1234. 	ADCQ	DX, R8

  1235. 	ADCQ	$0, R9

  1236. 

  1237. 	MOVQ	(64)(REG_P1), R14

  1238. 	MOVQ	(56)(REG_P2), AX

  1239. 	MULQ	R14

  1240. 	ADDQ	AX, R10

  1241. 	MOVQ	R10, (120)(CX)		// c3

  1242. 	ADCQ	DX, R8

  1243. 	ADCQ	$0, R9

  1244. 

  1245. 	XORQ	R10, R10

  1246. 	MOVQ	(80)(REG_P2), AX

  1247. 	MULQ	R11

  1248. 	ADDQ	AX, R8

  1249. 	ADCQ	DX, R9

  1250. 	ADCQ	$0, R10

  1251. 

  1252. 	MOVQ	(64)(REG_P2), AX

  1253. 	MULQ	R14

  1254. 	ADDQ	AX, R8

  1255. 	ADCQ	DX, R9

  1256. 	ADCQ	$0, R10

  1257. 

  1258. 	MOVQ	(80)(REG_P1), R15

  1259. 	MOVQ	R13, AX

  1260. 	MULQ	R15

  1261. 	ADDQ	AX, R8

  1262. 	ADCQ	DX, R9

  1263. 	ADCQ	$0, R10

  1264. 

  1265. 	MOVQ	(72)(REG_P2), AX

  1266. 	MULQ	R12

  1267. 	ADDQ	AX, R8

  1268. 	ADCQ	DX, R9

  1269. 	ADCQ	$0, R10

  1270. 

  1271. 	MOVQ	(72)(REG_P1), R13

  1272. 	MOVQ	(56)(REG_P2), AX

  1273. 	MULQ	R13

  1274. 	ADDQ	AX, R8

  1275. 	MOVQ	R8, (128)(CX)		// c4

  1276. 	ADCQ	DX, R9

  1277. 	ADCQ	$0, R10

  1278. 

  1279. 	XORQ	R8, R8

  1280. 	MOVQ	(88)(REG_P2), AX

  1281. 	MULQ	R11

  1282. 	ADDQ	AX, R9

  1283. 	ADCQ	DX, R10

  1284. 	ADCQ	$0, R8

  1285. 

  1286. 	MOVQ	(64)(REG_P2), AX

  1287. 	MULQ	R13

  1288. 	ADDQ	AX, R9

  1289. 	ADCQ	DX, R10

  1290. 	ADCQ	$0, R8

  1291. 

  1292. 	MOVQ	(72)(REG_P2), AX

  1293. 	MULQ	R14

  1294. 	ADDQ	AX, R9

  1295. 	ADCQ	DX, R10

  1296. 	ADCQ	$0, R8

  1297. 

  1298. 	MOVQ	(88)(REG_P1), R11

  1299. 	MOVQ	(48)(REG_P2), AX

  1300. 	MULQ	R11

  1301. 	ADDQ	AX, R9

  1302. 	ADCQ	DX, R10

  1303. 	ADCQ	$0, R8

  1304. 

  1305. 	MOVQ	(80)(REG_P2), AX

  1306. 	MULQ	R12

  1307. 	ADDQ	AX, R9

  1308. 	ADCQ	DX, R10

  1309. 	ADCQ	$0, R8

  1310. 

  1311. 	MOVQ	(56)(REG_P2), AX

  1312. 	MULQ	R15

  1313. 	ADDQ	AX, R9

  1314. 	MOVQ	R9, (136)(CX)		// c5

  1315. 	ADCQ	DX, R10

  1316. 	ADCQ	$0, R8

  1317. 

  1318. 	XORQ	R9, R9

  1319. 	MOVQ	(64)(REG_P2), AX

  1320. 	MULQ	R15

  1321. 	ADDQ	AX, R10

  1322. 	ADCQ	DX, R8

  1323. 	ADCQ	$0, R9

  1324. 

  1325. 	MOVQ	(88)(REG_P2), AX

  1326. 	MULQ	R12

  1327. 	ADDQ	AX, R10

  1328. 	ADCQ	DX, R8

  1329. 	ADCQ	$0, R9

  1330. 

  1331. 	MOVQ	(80)(REG_P2), AX

  1332. 	MULQ	R14

  1333. 	ADDQ	AX, R10

  1334. 	ADCQ	DX, R8

  1335. 	ADCQ	$0, R9

  1336. 

  1337. 	MOVQ	(56)(REG_P2), AX

  1338. 	MULQ	R11

  1339. 	ADDQ	AX, R10

  1340. 	ADCQ	DX, R8

  1341. 	ADCQ	$0, R9

  1342. 

  1343. 	MOVQ	(72)(REG_P2), AX

  1344. 	MULQ	R13

  1345. 	ADDQ	AX, R10

  1346. 	MOVQ	R10, (144)(CX)		// c6

  1347. 	ADCQ	DX, R8

  1348. 	ADCQ	$0, R9

  1349. 

  1350. 	XORQ	R10, R10

  1351. 	MOVQ	(88)(REG_P2), AX

  1352. 	MULQ	R14

  1353. 	ADDQ	AX, R8

  1354. 	ADCQ	DX, R9

  1355. 	ADCQ	$0, R10

  1356. 

  1357. 	MOVQ	(64)(REG_P2), AX

  1358. 	MULQ	R11

  1359. 	ADDQ	AX, R8

  1360. 	ADCQ	DX, R9

  1361. 	ADCQ	$0, R10

  1362. 

  1363. 	MOVQ	(80)(REG_P2), AX

  1364. 	MULQ	R13

  1365. 	ADDQ	AX, R8

  1366. 	ADCQ	DX, R9

  1367. 	ADCQ	$0, R10

  1368. 

  1369. 	MOVQ	(72)(REG_P2), AX

  1370. 	MULQ	R15

  1371. 	ADDQ	AX, R8

  1372. 	MOVQ	R8, (152)(CX)		// c7

  1373. 	ADCQ	DX, R9

  1374. 	ADCQ	$0, R10

  1375. 

  1376. 	XORQ	R8, R8

  1377. 	MOVQ	(72)(REG_P2), AX

  1378. 	MULQ	R11

  1379. 	ADDQ	AX, R9

  1380. 	ADCQ	DX, R10

  1381. 	ADCQ	$0, R8

  1382. 

  1383. 	MOVQ	(80)(REG_P2), AX

  1384. 	MULQ	R15

  1385. 	ADDQ	AX, R9

  1386. 	ADCQ	DX, R10

  1387. 	ADCQ	$0, R8

  1388. 

  1389. 	MOVQ	(88)(REG_P2), AX

  1390. 	MULQ	R13

  1391. 	ADDQ	AX, R9

  1392. 	MOVQ	R9, (160)(CX)		// c8

  1393. 	ADCQ	DX, R10

  1394. 	ADCQ	$0, R8

  1395. 

  1396. 	MOVQ	(88)(REG_P2), AX

  1397. 	MULQ	R15

  1398. 	ADDQ	AX, R10

  1399. 	ADCQ	DX, R8

  1400. 

  1401. 	MOVQ	(80)(REG_P2), AX

  1402. 	MULQ	R11

  1403. 	ADDQ	AX, R10

  1404. 	MOVQ	R10, (168)(CX)		// c9

  1405. 	ADCQ	DX, R8

  1406. 

  1407. 	MOVQ	(88)(REG_P2), AX

  1408. 	MULQ	R11

  1409. 	ADDQ	AX, R8

  1410. 	MOVQ	R8, (176)(CX)		// c10

  1411. 	ADCQ	$0, DX

  1412. 	MOVQ	DX, (184)(CX)		// c11

  1413. 

  1414. 	// [R8-R15,AX,DX,DI,(SP)] <- (AH+AL)*(BH+BL)-AL*BL

  1415. 	MOVQ	(SP), R8

  1416. 	SUBQ	(CX), R8

  1417. 	MOVQ	(8)(SP), R9

  1418. 	SBBQ	(8)(CX), R9

  1419. 	MOVQ	(16)(SP), R10

  1420. 	SBBQ	(16)(CX), R10

  1421. 	MOVQ	(24)(SP), R11

  1422. 	SBBQ	(24)(CX), R11

  1423. 	MOVQ	(32)(SP), R12

  1424. 	SBBQ	(32)(CX), R12

  1425. 	MOVQ	(40)(SP), R13

  1426. 	SBBQ	(40)(CX), R13

  1427. 	MOVQ	(48)(SP), R14

  1428. 	SBBQ	(48)(CX), R14

  1429. 	MOVQ	(56)(SP), R15

  1430. 	SBBQ	(56)(CX), R15

  1431. 	MOVQ	(64)(SP), AX

  1432. 	SBBQ	(64)(CX), AX

  1433. 	MOVQ	(72)(SP), DX

  1434. 	SBBQ	(72)(CX), DX

  1435. 	MOVQ	(80)(SP), DI

  1436. 	SBBQ	(80)(CX), DI

  1437. 	MOVQ	(88)(SP), SI

  1438. 	SBBQ	(88)(CX), SI

  1439. 	MOVQ	SI, (SP)

  1440. 

  1441. 	// [R8-R15,AX,DX,DI,(SP)] <- (AH+AL)*(BH+BL) - AL*BL - AH*BH

  1442. 	MOVQ	(96)(CX), SI

  1443. 	SUBQ	SI, R8

  1444. 	MOVQ	(104)(CX), SI

  1445. 	SBBQ	SI, R9

  1446. 	MOVQ	(112)(CX), SI

  1447. 	SBBQ	SI, R10

  1448. 	MOVQ	(120)(CX), SI

  1449. 	SBBQ	SI, R11

  1450. 	MOVQ	(128)(CX), SI

  1451. 	SBBQ	SI, R12

  1452. 	MOVQ	(136)(CX), SI

  1453. 	SBBQ	SI, R13

  1454. 	MOVQ	(144)(CX), SI

  1455. 	SBBQ	SI, R14

  1456. 	MOVQ	(152)(CX), SI

  1457. 	SBBQ	SI, R15

  1458. 	MOVQ	(160)(CX), SI

  1459. 	SBBQ	SI, AX

  1460. 	MOVQ	(168)(CX), SI

  1461. 	SBBQ	SI, DX

  1462. 	MOVQ	(176)(CX), SI

  1463. 	SBBQ	SI, DI

  1464. 	MOVQ	(SP), SI

  1465. 	SBBQ	(184)(CX), SI

  1466. 

  1467. 	// FINAL RESULT

  1468. 	ADDQ	(48)(CX), R8

  1469. 	MOVQ	R8, (48)(CX)

  1470. 	ADCQ	(56)(CX), R9

  1471. 	MOVQ	R9, (56)(CX)

  1472. 	ADCQ	(64)(CX), R10

  1473. 	MOVQ	R10, (64)(CX)

  1474. 	ADCQ	(72)(CX), R11

  1475. 	MOVQ	R11, (72)(CX)

  1476. 	ADCQ	(80)(CX), R12

  1477. 	MOVQ	R12, (80)(CX)

  1478. 	ADCQ	(88)(CX), R13

  1479. 	MOVQ	R13, (88)(CX)

  1480. 	ADCQ	(96)(CX), R14

  1481. 	MOVQ	R14, (96)(CX)

  1482. 	ADCQ	(104)(CX), R15

  1483. 	MOVQ	R15, (104)(CX)

  1484. 	ADCQ	(112)(CX), AX

  1485. 	MOVQ	AX, (112)(CX)

  1486. 	ADCQ	(120)(CX), DX

  1487. 	MOVQ	DX, (120)(CX)

  1488. 	ADCQ	(128)(CX), DI

  1489. 	MOVQ	DI, (128)(CX)

  1490. 	ADCQ	(136)(CX), SI

  1491. 	MOVQ	SI, (136)(CX)

  1492. 	MOVQ	(144)(CX), AX

  1493. 	ADCQ	$0, AX

  1494. 	MOVQ	AX, (144)(CX)

  1495. 	MOVQ	(152)(CX), AX

  1496. 	ADCQ	$0, AX

  1497. 	MOVQ	AX, (152)(CX)

  1498. 	MOVQ	(160)(CX), AX

  1499. 	ADCQ	$0, AX

  1500. 	MOVQ	AX, (160)(CX)

  1501. 	MOVQ	(168)(CX), AX

  1502. 	ADCQ	$0, AX

  1503. 	MOVQ	AX, (168)(CX)

  1504. 	MOVQ	(176)(CX), AX

  1505. 	ADCQ	$0, AX

  1506. 	MOVQ	AX, (176)(CX)

  1507. 	MOVQ	(184)(CX), AX

  1508. 	ADCQ	$0, AX

  1509. 	MOVQ	AX, (184)(CX)

  1510. 

  1511. 	RET

  1512. 

  1513. TEXT ·fp751MontgomeryReduce(SB), $0-16

  1514. 

  1515. 	MOVQ z+0(FP), REG_P2

  1516. 	MOVQ x+8(FP), REG_P1

  1517. 

  1518. 	MOVQ	(REG_P1), R11

  1519. 	MOVQ	P751P1_5, AX

  1520. 	MULQ	R11

  1521. 	XORQ	R8, R8

  1522. 	ADDQ	(40)(REG_P1), AX

  1523. 	MOVQ	AX, (40)(REG_P2)		// Z5

  1524. 	ADCQ	DX, R8

  1525. 

  1526. 	XORQ	R9, R9

  1527. 	MOVQ	P751P1_6, AX

  1528. 	MULQ	R11

  1529. 	XORQ	R10, R10

  1530. 	ADDQ	AX, R8

  1531. 	ADCQ	DX, R9

  1532. 

  1533. 	MOVQ	(8)(REG_P1), R12

  1534. 	MOVQ	P751P1_5, AX

  1535. 	MULQ	R12

  1536. 	ADDQ	AX, R8

  1537. 	ADCQ	DX, R9

  1538. 	ADCQ	$0, R10

  1539. 	ADDQ	(48)(REG_P1), R8

  1540. 	MOVQ	R8, (48)(REG_P2)		// Z6

  1541. 	ADCQ	$0, R9

  1542. 	ADCQ	$0, R10

  1543. 

  1544. 	XORQ	R8, R8

  1545. 	MOVQ	P751P1_7, AX

  1546. 	MULQ	R11

  1547. 	ADDQ	AX, R9

  1548. 	ADCQ	DX, R10

  1549. 	ADCQ	$0, R8

  1550. 

  1551. 	MOVQ	P751P1_6, AX

  1552. 	MULQ	R12

  1553. 	ADDQ	AX, R9

  1554. 	ADCQ	DX, R10

  1555. 	ADCQ	$0, R8

  1556. 

  1557. 	MOVQ	(16)(REG_P1), R13

  1558. 	MOVQ	P751P1_5, AX

  1559. 	MULQ	R13

  1560. 	ADDQ	AX, R9

  1561. 	ADCQ	DX, R10

  1562. 	ADCQ	$0, R8

  1563. 	ADDQ	(56)(REG_P1), R9

  1564. 	MOVQ	R9, (56)(REG_P2)		// Z7

  1565. 	ADCQ	$0, R10

  1566. 	ADCQ	$0, R8

  1567. 

  1568. 	XORQ	R9, R9

  1569. 	MOVQ	P751P1_8, AX

  1570. 	MULQ	R11

  1571. 	ADDQ	AX, R10

  1572. 	ADCQ	DX, R8

  1573. 	ADCQ	$0, R9

  1574. 

  1575. 	MOVQ	P751P1_7, AX

  1576. 	MULQ	R12

  1577. 	ADDQ	AX, R10

  1578. 	ADCQ	DX, R8

  1579. 	ADCQ	$0, R9

  1580. 

  1581. 	MOVQ	P751P1_6, AX

  1582. 	MULQ	R13

  1583. 	ADDQ	AX, R10

  1584. 	ADCQ	DX, R8

  1585. 	ADCQ	$0, R9

  1586. 

  1587. 	MOVQ	(24)(REG_P1), R14

  1588. 	MOVQ	P751P1_5, AX

  1589. 	MULQ	R14

  1590. 	ADDQ	AX, R10

  1591. 	ADCQ	DX, R8

  1592. 	ADCQ	$0, R9

  1593. 	ADDQ	(64)(REG_P1), R10

  1594. 	MOVQ	R10, (64)(REG_P2)		// Z8

  1595. 	ADCQ	$0, R8

  1596. 	ADCQ	$0, R9

  1597. 

  1598. 	XORQ	R10, R10

  1599. 	MOVQ	P751P1_9, AX

  1600. 	MULQ	R11

  1601. 	ADDQ	AX, R8

  1602. 	ADCQ	DX, R9

  1603. 	ADCQ	$0, R10

  1604. 

  1605. 	MOVQ	P751P1_8, AX

  1606. 	MULQ	R12

  1607. 	ADDQ	AX, R8

  1608. 	ADCQ	DX, R9

  1609. 	ADCQ	$0, R10

  1610. 

  1611. 	MOVQ	P751P1_7, AX

  1612. 	MULQ	R13

  1613. 	ADDQ	AX, R8

  1614. 	ADCQ	DX, R9

  1615. 	ADCQ	$0, R10

  1616. 

  1617. 	MOVQ	P751P1_6, AX

  1618. 	MULQ	R14

  1619. 	ADDQ	AX, R8

  1620. 	ADCQ	DX, R9

  1621. 	ADCQ	$0, R10

  1622. 

  1623. 	MOVQ	(32)(REG_P1), R15

  1624. 	MOVQ	P751P1_5, AX

  1625. 	MULQ	R15

  1626. 	ADDQ	AX, R8

  1627. 	ADCQ	DX, R9

  1628. 	ADCQ	$0, R10

  1629. 	ADDQ	(72)(REG_P1), R8

  1630. 	MOVQ	R8, (72)(REG_P2)		// Z9

  1631. 	ADCQ	$0, R9

  1632. 	ADCQ	$0, R10

  1633. 

  1634. 	XORQ	R8, R8

  1635. 	MOVQ	P751P1_10, AX

  1636. 	MULQ	R11

  1637. 	ADDQ	AX, R9

  1638. 	ADCQ	DX, R10

  1639. 	ADCQ	$0, R8

  1640. 

  1641. 	MOVQ	P751P1_9, AX

  1642. 	MULQ	R12

  1643. 	ADDQ	AX, R9

  1644. 	ADCQ	DX, R10

  1645. 	ADCQ	$0, R8

  1646. 

  1647. 	MOVQ	P751P1_8, AX

  1648. 	MULQ	R13

  1649. 	ADDQ	AX, R9

  1650. 	ADCQ	DX, R10

  1651. 	ADCQ	$0, R8

  1652. 

  1653. 	MOVQ	P751P1_7, AX

  1654. 	MULQ	R14

  1655. 	ADDQ	AX, R9

  1656. 	ADCQ	DX, R10

  1657. 	ADCQ	$0, R8

  1658. 

  1659. 	MOVQ	P751P1_6, AX

  1660. 	MULQ	R15

  1661. 	ADDQ	AX, R9

  1662. 	ADCQ	DX, R10

  1663. 	ADCQ	$0, R8

  1664. 

  1665. 	MOVQ	(40)(REG_P2), CX

  1666. 	MOVQ	P751P1_5, AX

  1667. 	MULQ	CX

  1668. 	ADDQ	AX, R9

  1669. 	ADCQ	DX, R10

  1670. 	ADCQ	$0, R8

  1671. 	ADDQ	(80)(REG_P1), R9

  1672. 	MOVQ	R9, (80)(REG_P2)		// Z10

  1673. 	ADCQ	$0, R10

  1674. 	ADCQ	$0, R8

  1675. 

  1676. 	XORQ	R9, R9

  1677. 	MOVQ	P751P1_11, AX

  1678. 	MULQ	R11

  1679. 	ADDQ	AX, R10

  1680. 	ADCQ	DX, R8

  1681. 	ADCQ	$0, R9

  1682. 

  1683. 	MOVQ	P751P1_10, AX

  1684. 	MULQ	R12

  1685. 	ADDQ	AX, R10

  1686. 	ADCQ	DX, R8

  1687. 	ADCQ	$0, R9

  1688. 

  1689. 	MOVQ	P751P1_9, AX

  1690. 	MULQ	R13

  1691. 	ADDQ	AX, R10

  1692. 	ADCQ	DX, R8

  1693. 	ADCQ	$0, R9

  1694. 

  1695. 	MOVQ	P751P1_8, AX

  1696. 	MULQ	R14

  1697. 	ADDQ	AX, R10

  1698. 	ADCQ	DX, R8

  1699. 	ADCQ	$0, R9

  1700. 

  1701. 	MOVQ	P751P1_7, AX

  1702. 	MULQ	R15

  1703. 	ADDQ	AX, R10

  1704. 	ADCQ	DX, R8

  1705. 	ADCQ	$0, R9

  1706. 

  1707. 	MOVQ	P751P1_6, AX

  1708. 	MULQ	CX

  1709. 	ADDQ	AX, R10

  1710. 	ADCQ	DX, R8

  1711. 	ADCQ	$0, R9

  1712. 

  1713. 	MOVQ	(48)(REG_P2), R11

  1714. 	MOVQ	P751P1_5, AX

  1715. 	MULQ	R11

  1716. 	ADDQ	AX, R10

  1717. 	ADCQ	DX, R8

  1718. 	ADCQ	$0, R9

  1719. 	ADDQ	(88)(REG_P1), R10

  1720. 	MOVQ	R10, (88)(REG_P2)		// Z11

  1721. 	ADCQ	$0, R8

  1722. 	ADCQ	$0, R9

  1723. 

  1724. 	XORQ	R10, R10

  1725. 	MOVQ	P751P1_11, AX

  1726. 	MULQ	R12

  1727. 	ADDQ	AX, R8

  1728. 	ADCQ	DX, R9

  1729. 	ADCQ	$0, R10

  1730. 

  1731. 	MOVQ	P751P1_10, AX

  1732. 	MULQ	R13

  1733. 	ADDQ	AX, R8

  1734. 	ADCQ	DX, R9

  1735. 	ADCQ	$0, R10

  1736. 

  1737. 	MOVQ	P751P1_9, AX

  1738. 	MULQ	R14

  1739. 	ADDQ	AX, R8

  1740. 	ADCQ	DX, R9

  1741. 	ADCQ	$0, R10

  1742. 

  1743. 	MOVQ	P751P1_8, AX

  1744. 	MULQ	R15

  1745. 	ADDQ	AX, R8

  1746. 	ADCQ	DX, R9

  1747. 	ADCQ	$0, R10

  1748. 

  1749. 	MOVQ	P751P1_7, AX

  1750. 	MULQ	CX

  1751. 	ADDQ	AX, R8

  1752. 	ADCQ	DX, R9

  1753. 	ADCQ	$0, R10

  1754. 

  1755. 	MOVQ	P751P1_6, AX

  1756. 	MULQ	R11

  1757. 	ADDQ	AX, R8

  1758. 	ADCQ	DX, R9

  1759. 	ADCQ	$0, R10

  1760. 

  1761. 	MOVQ	(56)(REG_P2), R12

  1762. 	MOVQ	P751P1_5, AX

  1763. 	MULQ	R12

  1764. 	ADDQ	AX, R8

  1765. 	ADCQ	DX, R9

  1766. 	ADCQ	$0, R10

  1767. 	ADDQ	(96)(REG_P1), R8

  1768. 	MOVQ	R8, (REG_P2)		// Z0

  1769. 	ADCQ	$0, R9

  1770. 	ADCQ	$0, R10

  1771. 

  1772. 	XORQ	R8, R8

  1773. 	MOVQ	P751P1_11, AX

  1774. 	MULQ	R13

  1775. 	ADDQ	AX, R9

  1776. 	ADCQ	DX, R10

  1777. 	ADCQ	$0, R8

  1778. 

  1779. 	MOVQ	P751P1_10, AX

  1780. 	MULQ	R14

  1781. 	ADDQ	AX, R9

  1782. 	ADCQ	DX, R10

  1783. 	ADCQ	$0, R8

  1784. 

  1785. 	MOVQ	P751P1_9, AX

  1786. 	MULQ	R15

  1787. 	ADDQ	AX, R9

  1788. 	ADCQ	DX, R10

  1789. 	ADCQ	$0, R8

  1790. 

  1791. 	MOVQ	P751P1_8, AX

  1792. 	MULQ	CX

  1793. 	ADDQ	AX, R9

  1794. 	ADCQ	DX, R10

  1795. 	ADCQ	$0, R8

  1796. 

  1797. 	MOVQ	P751P1_7, AX

  1798. 	MULQ	R11

  1799. 	ADDQ	AX, R9

  1800. 	ADCQ	DX, R10

  1801. 	ADCQ	$0, R8

  1802. 

  1803. 	MOVQ	P751P1_6, AX

  1804. 	MULQ	R12

  1805. 	ADDQ	AX, R9

  1806. 	ADCQ	DX, R10

  1807. 	ADCQ	$0, R8

  1808. 

  1809. 	MOVQ	(64)(REG_P2), R13

  1810. 	MOVQ	P751P1_5, AX

  1811. 	MULQ	R13

  1812. 	ADDQ	AX, R9

  1813. 	ADCQ	DX, R10

  1814. 	ADCQ	$0, R8

  1815. 	ADDQ	(104)(REG_P1), R9

  1816. 	MOVQ	R9, (8)(REG_P2)		// Z1

  1817. 	ADCQ	$0, R10

  1818. 	ADCQ	$0, R8

  1819. 

  1820. 	XORQ	R9, R9

  1821. 	MOVQ	P751P1_11, AX

  1822. 	MULQ	R14

  1823. 	ADDQ	AX, R10

  1824. 	ADCQ	DX, R8

  1825. 	ADCQ	$0, R9

  1826. 

  1827. 	MOVQ	P751P1_10, AX

  1828. 	MULQ	R15

  1829. 	ADDQ	AX, R10

  1830. 	ADCQ	DX, R8

  1831. 	ADCQ	$0, R9

  1832. 

  1833. 	MOVQ	P751P1_9, AX

  1834. 	MULQ	CX

  1835. 	ADDQ	AX, R10

  1836. 	ADCQ	DX, R8

  1837. 	ADCQ	$0, R9

  1838. 

  1839. 	MOVQ	P751P1_8, AX

  1840. 	MULQ	R11

  1841. 	ADDQ	AX, R10

  1842. 	ADCQ	DX, R8

  1843. 	ADCQ	$0, R9

  1844. 

  1845. 	MOVQ	P751P1_7, AX

  1846. 	MULQ	R12

  1847. 	ADDQ	AX, R10

  1848. 	ADCQ	DX, R8

  1849. 	ADCQ	$0, R9

  1850. 

  1851. 	MOVQ	P751P1_6, AX

  1852. 	MULQ	R13

  1853. 	ADDQ	AX, R10

  1854. 	ADCQ	DX, R8

  1855. 	ADCQ	$0, R9

  1856. 

  1857. 	MOVQ	(72)(REG_P2), R14

  1858. 	MOVQ	P751P1_5, AX

  1859. 	MULQ	R14

  1860. 	ADDQ	AX, R10

  1861. 	ADCQ	DX, R8

  1862. 	ADCQ	$0, R9

  1863. 	ADDQ	(112)(REG_P1), R10

  1864. 	MOVQ	R10, (16)(REG_P2)		// Z2

  1865. 	ADCQ	$0, R8

  1866. 	ADCQ	$0, R9

  1867. 

  1868. 	XORQ	R10, R10

  1869. 	MOVQ	P751P1_11, AX

  1870. 	MULQ	R15

  1871. 	ADDQ	AX, R8

  1872. 	ADCQ	DX, R9

  1873. 	ADCQ	$0, R10

  1874. 

  1875. 	MOVQ	P751P1_10, AX

  1876. 	MULQ	CX

  1877. 	ADDQ	AX, R8

  1878. 	ADCQ	DX, R9

  1879. 	ADCQ	$0, R10

  1880. 

  1881. 	MOVQ	P751P1_9, AX

  1882. 	MULQ	R11

  1883. 	ADDQ	AX, R8

  1884. 	ADCQ	DX, R9

  1885. 	ADCQ	$0, R10

  1886. 

  1887. 	MOVQ	P751P1_8, AX

  1888. 	MULQ	R12

  1889. 	ADDQ	AX, R8

  1890. 	ADCQ	DX, R9

  1891. 	ADCQ	$0, R10

  1892. 

  1893. 	MOVQ	P751P1_7, AX

  1894. 	MULQ	R13

  1895. 	ADDQ	AX, R8

  1896. 	ADCQ	DX, R9

  1897. 	ADCQ	$0, R10

  1898. 

  1899. 	MOVQ	P751P1_6, AX

  1900. 	MULQ	R14

  1901. 	ADDQ	AX, R8

  1902. 	ADCQ	DX, R9

  1903. 	ADCQ	$0, R10

  1904. 

  1905. 	MOVQ	(80)(REG_P2), R15

  1906. 	MOVQ	P751P1_5, AX

  1907. 	MULQ	R15

  1908. 	ADDQ	AX, R8

  1909. 	ADCQ	DX, R9

  1910. 	ADCQ	$0, R10

  1911. 	ADDQ	(120)(REG_P1), R8

  1912. 	MOVQ	R8, (24)(REG_P2)		// Z3

  1913. 	ADCQ	$0, R9

  1914. 	ADCQ	$0, R10

  1915. 

  1916. 	XORQ	R8, R8

  1917. 	MOVQ	P751P1_11, AX

  1918. 	MULQ	CX

  1919. 	ADDQ	AX, R9

  1920. 	ADCQ	DX, R10

  1921. 	ADCQ	$0, R8

  1922. 

  1923. 	MOVQ	P751P1_10, AX

  1924. 	MULQ	R11

  1925. 	ADDQ	AX, R9

  1926. 	ADCQ	DX, R10

  1927. 	ADCQ	$0, R8

  1928. 

  1929. 	MOVQ	P751P1_9, AX

  1930. 	MULQ	R12

  1931. 	ADDQ	AX, R9

  1932. 	ADCQ	DX, R10

  1933. 	ADCQ	$0, R8

  1934. 

  1935. 	MOVQ	P751P1_8, AX

  1936. 	MULQ	R13

  1937. 	ADDQ	AX, R9

  1938. 	ADCQ	DX, R10

  1939. 	ADCQ	$0, R8

  1940. 

  1941. 	MOVQ	P751P1_7, AX

  1942. 	MULQ	R14

  1943. 	ADDQ	AX, R9

  1944. 	ADCQ	DX, R10

  1945. 	ADCQ	$0, R8

  1946. 

  1947. 	MOVQ	P751P1_6, AX

  1948. 	MULQ	R15

  1949. 	ADDQ	AX, R9

  1950. 	ADCQ	DX, R10

  1951. 	ADCQ	$0, R8

  1952. 

  1953. 	MOVQ	(88)(REG_P2), CX

  1954. 	MOVQ	P751P1_5, AX

  1955. 	MULQ	CX

  1956. 	ADDQ	AX, R9

  1957. 	ADCQ	DX, R10

  1958. 	ADCQ	$0, R8

  1959. 	ADDQ	(128)(REG_P1), R9

  1960. 	MOVQ	R9, (32)(REG_P2)		// Z4

  1961. 	ADCQ	$0, R10

  1962. 	ADCQ	$0, R8

  1963. 

  1964. 	XORQ	R9, R9

  1965. 	MOVQ	P751P1_11, AX

  1966. 	MULQ	R11

  1967. 	ADDQ	AX, R10

  1968. 	ADCQ	DX, R8

  1969. 	ADCQ	$0, R9

  1970. 

  1971. 	MOVQ	P751P1_10, AX

  1972. 	MULQ	R12

  1973. 	ADDQ	AX, R10

  1974. 	ADCQ	DX, R8

  1975. 	ADCQ	$0, R9

  1976. 

  1977. 	MOVQ	P751P1_9, AX

  1978. 	MULQ	R13

  1979. 	ADDQ	AX, R10

  1980. 	ADCQ	DX, R8

  1981. 	ADCQ	$0, R9

  1982. 

  1983. 	MOVQ	P751P1_8, AX

  1984. 	MULQ	R14

  1985. 	ADDQ	AX, R10

  1986. 	ADCQ	DX, R8

  1987. 	ADCQ	$0, R9

  1988. 

  1989. 	MOVQ	P751P1_7, AX

  1990. 	MULQ	R15

  1991. 	ADDQ	AX, R10

  1992. 	ADCQ	DX, R8

  1993. 	ADCQ	$0, R9

  1994. 

  1995. 	MOVQ	P751P1_6, AX

  1996. 	MULQ	CX

  1997. 	ADDQ	AX, R10

  1998. 	ADCQ	DX, R8

  1999. 	ADCQ	$0, R9

  2000. 	ADDQ	(136)(REG_P1), R10

  2001. 	MOVQ	R10, (40)(REG_P2)		// Z5

  2002. 	ADCQ	$0, R8

  2003. 	ADCQ	$0, R9

  2004. 

  2005. 	XORQ	R10, R10

  2006. 	MOVQ	P751P1_11, AX

  2007. 	MULQ	R12

  2008. 	ADDQ	AX, R8

  2009. 	ADCQ	DX, R9

  2010. 	ADCQ	$0, R10

  2011. 

  2012. 	MOVQ	P751P1_10, AX

  2013. 	MULQ	R13

  2014. 	ADDQ	AX, R8

  2015. 	ADCQ	DX, R9

  2016. 	ADCQ	$0, R10

  2017. 

  2018. 	MOVQ	P751P1_9, AX

  2019. 	MULQ	R14

  2020. 	ADDQ	AX, R8

  2021. 	ADCQ	DX, R9

  2022. 	ADCQ	$0, R10

  2023. 

  2024. 	MOVQ	P751P1_8, AX

  2025. 	MULQ	R15

  2026. 	ADDQ	AX, R8

  2027. 	ADCQ	DX, R9

  2028. 	ADCQ	$0, R10

  2029. 

  2030. 	MOVQ	P751P1_7, AX

  2031. 	MULQ	CX

  2032. 	ADDQ	AX, R8

  2033. 	ADCQ	DX, R9

  2034. 	ADCQ	$0, R10

  2035. 	ADDQ	(144)(REG_P1), R8

  2036. 	MOVQ	R8, (48)(REG_P2)		// Z6

  2037. 	ADCQ	$0, R9

  2038. 	ADCQ	$0, R10

  2039. 

  2040. 	XORQ	R8, R8

  2041. 	MOVQ	P751P1_11, AX

  2042. 	MULQ	R13

  2043. 	ADDQ	AX, R9

  2044. 	ADCQ	DX, R10

  2045. 	ADCQ	$0, R8

  2046. 

  2047. 	MOVQ	P751P1_10, AX

  2048. 	MULQ	R14

  2049. 	ADDQ	AX, R9

  2050. 	ADCQ	DX, R10

  2051. 	ADCQ	$0, R8

  2052. 

  2053. 	MOVQ	P751P1_9, AX

  2054. 	MULQ	R15

  2055. 	ADDQ	AX, R9

  2056. 	ADCQ	DX, R10

  2057. 	ADCQ	$0, R8

  2058. 

  2059. 	MOVQ	P751P1_8, AX

  2060. 	MULQ	CX

  2061. 	ADDQ	AX, R9

  2062. 	ADCQ	DX, R10

  2063. 	ADCQ	$0, R8

  2064. 	ADDQ	(152)(REG_P1), R9

  2065. 	MOVQ	R9, (56)(REG_P2)		// Z7

  2066. 	ADCQ	$0, R10

  2067. 	ADCQ	$0, R8

  2068. 

  2069. 	XORQ	R9, R9

  2070. 	MOVQ	P751P1_11, AX

  2071. 	MULQ	R14

  2072. 	ADDQ	AX, R10

  2073. 	ADCQ	DX, R8

  2074. 	ADCQ	$0, R9

  2075. 

  2076. 	MOVQ	P751P1_10, AX

  2077. 	MULQ	R15

  2078. 	ADDQ	AX, R10

  2079. 	ADCQ	DX, R8

  2080. 	ADCQ	$0, R9

  2081. 

  2082. 	MOVQ	P751P1_9, AX

  2083. 	MULQ	CX

  2084. 	ADDQ	AX, R10

  2085. 	ADCQ	DX, R8

  2086. 	ADCQ	$0, R9

  2087. 	ADDQ	(160)(REG_P1), R10

  2088. 	MOVQ	R10, (64)(REG_P2)		// Z8

  2089. 	ADCQ	$0, R8

  2090. 	ADCQ	$0, R9

  2091. 

  2092. 	XORQ	R10, R10

  2093. 	MOVQ	P751P1_11, AX

  2094. 	MULQ	R15

  2095. 	ADDQ	AX, R8

  2096. 	ADCQ	DX, R9

  2097. 	ADCQ	$0, R10

  2098. 

  2099. 	MOVQ	P751P1_10, AX

  2100. 	MULQ	CX

  2101. 	ADDQ	AX, R8

  2102. 	ADCQ	DX, R9

  2103. 	ADCQ	$0, R10

  2104. 	ADDQ	(168)(REG_P1), R8		// Z9

  2105. 	MOVQ	R8, (72)(REG_P2)		// Z9

  2106. 	ADCQ	$0, R9

  2107. 	ADCQ	$0, R10

  2108. 

  2109. 	MOVQ	P751P1_11, AX

  2110. 	MULQ	CX

  2111. 	ADDQ	AX, R9

  2112. 	ADCQ	DX, R10

  2113. 	ADDQ	(176)(REG_P1), R9		// Z10

  2114. 	MOVQ	R9, (80)(REG_P2)		// Z10

  2115. 	ADCQ	$0, R10

  2116. 	ADDQ	(184)(REG_P1), R10		// Z11

  2117. 	MOVQ	R10, (88)(REG_P2)		// Z11

  2118. 

  2119. 	RET

  2120. 

  2121. TEXT ·fp751AddLazy(SB), NOSPLIT, $0-24

  2122. 

  2123. 	MOVQ z+0(FP), REG_P3

  2124. 	MOVQ x+8(FP), REG_P1

  2125. 	MOVQ y+16(FP), REG_P2

  2126. 

  2127. 	MOVQ	(REG_P1), R8

  2128. 	MOVQ	(8)(REG_P1), R9

  2129. 	MOVQ	(16)(REG_P1), R10

  2130. 	MOVQ	(24)(REG_P1), R11

  2131. 	MOVQ	(32)(REG_P1), R12

  2132. 	MOVQ	(40)(REG_P1), R13

  2133. 	MOVQ	(48)(REG_P1), R14

  2134. 	MOVQ	(56)(REG_P1), R15

  2135. 	MOVQ	(64)(REG_P1), AX

  2136. 	MOVQ	(72)(REG_P1), BX

  2137. 	MOVQ	(80)(REG_P1), CX

  2138. 	MOVQ	(88)(REG_P1), DI

  2139. 

  2140. 	ADDQ	(REG_P2), R8

  2141. 	ADCQ	(8)(REG_P2), R9

  2142. 	ADCQ	(16)(REG_P2), R10

  2143. 	ADCQ	(24)(REG_P2), R11

  2144. 	ADCQ	(32)(REG_P2), R12

  2145. 	ADCQ	(40)(REG_P2), R13

  2146. 	ADCQ	(48)(REG_P2), R14

  2147. 	ADCQ	(56)(REG_P2), R15

  2148. 	ADCQ	(64)(REG_P2), AX

  2149. 	ADCQ	(72)(REG_P2), BX

  2150. 	ADCQ	(80)(REG_P2), CX

  2151. 	ADCQ	(88)(REG_P2), DI

  2152. 

  2153. 	MOVQ	R8, (REG_P3)

  2154. 	MOVQ	R9, (8)(REG_P3)

  2155. 	MOVQ	R10, (16)(REG_P3)

  2156. 	MOVQ	R11, (24)(REG_P3)

  2157. 	MOVQ	R12, (32)(REG_P3)

  2158. 	MOVQ	R13, (40)(REG_P3)

  2159. 	MOVQ	R14, (48)(REG_P3)

  2160. 	MOVQ	R15, (56)(REG_P3)

  2161. 	MOVQ	AX, (64)(REG_P3)

  2162. 	MOVQ	BX, (72)(REG_P3)

  2163. 	MOVQ	CX, (80)(REG_P3)

  2164. 	MOVQ	DI, (88)(REG_P3)

  2165. 

  2166. 	RET

  2167. 

  2168. TEXT ·fp751X2AddLazy(SB), NOSPLIT, $0-24

  2169. 

  2170. 	MOVQ z+0(FP), REG_P3

  2171. 	MOVQ x+8(FP), REG_P1

  2172. 	MOVQ y+16(FP), REG_P2

  2173. 

  2174. 	MOVQ	(REG_P1), R8

  2175. 	MOVQ	(8)(REG_P1), R9

  2176. 	MOVQ	(16)(REG_P1), R10

  2177. 	MOVQ	(24)(REG_P1), R11

  2178. 	MOVQ	(32)(REG_P1), R12

  2179. 	MOVQ	(40)(REG_P1), R13

  2180. 	MOVQ	(48)(REG_P1), R14

  2181. 	MOVQ	(56)(REG_P1), R15

  2182. 	MOVQ	(64)(REG_P1), AX

  2183. 	MOVQ	(72)(REG_P1), BX

  2184. 	MOVQ	(80)(REG_P1), CX

  2185. 

  2186. 	ADDQ	(REG_P2), R8

  2187. 	ADCQ	(8)(REG_P2), R9

  2188. 	ADCQ	(16)(REG_P2), R10

  2189. 	ADCQ	(24)(REG_P2), R11

  2190. 	ADCQ	(32)(REG_P2), R12

  2191. 	ADCQ	(40)(REG_P2), R13

  2192. 	ADCQ	(48)(REG_P2), R14

  2193. 	ADCQ	(56)(REG_P2), R15

  2194. 	ADCQ	(64)(REG_P2), AX

  2195. 	ADCQ	(72)(REG_P2), BX

  2196. 	ADCQ	(80)(REG_P2), CX

  2197. 

  2198. 	MOVQ	R8, (REG_P3)

  2199. 	MOVQ	R9, (8)(REG_P3)

  2200. 	MOVQ	R10, (16)(REG_P3)

  2201. 	MOVQ	R11, (24)(REG_P3)

  2202. 	MOVQ	R12, (32)(REG_P3)

  2203. 	MOVQ	R13, (40)(REG_P3)

  2204. 	MOVQ	R14, (48)(REG_P3)

  2205. 	MOVQ	R15, (56)(REG_P3)

  2206. 	MOVQ	AX, (64)(REG_P3)

  2207. 	MOVQ	BX, (72)(REG_P3)

  2208. 	MOVQ	CX, (80)(REG_P3)

  2209. 	MOVQ	(88)(REG_P1), AX

  2210. 	ADCQ	(88)(REG_P2), AX

  2211. 	MOVQ	AX, (88)(REG_P3)

  2212. 

  2213. 	MOVQ	(96)(REG_P1), R8

  2214. 	MOVQ	(104)(REG_P1), R9

  2215. 	MOVQ	(112)(REG_P1), R10

  2216. 	MOVQ	(120)(REG_P1), R11

  2217. 	MOVQ	(128)(REG_P1), R12

  2218. 	MOVQ	(136)(REG_P1), R13

  2219. 	MOVQ	(144)(REG_P1), R14

  2220. 	MOVQ	(152)(REG_P1), R15

  2221. 	MOVQ	(160)(REG_P1), AX

  2222. 	MOVQ	(168)(REG_P1), BX

  2223. 	MOVQ	(176)(REG_P1), CX

  2224. 	MOVQ	(184)(REG_P1), DI

  2225. 

  2226. 	ADCQ	(96)(REG_P2), R8

  2227. 	ADCQ	(104)(REG_P2), R9

  2228. 	ADCQ	(112)(REG_P2), R10

  2229. 	ADCQ	(120)(REG_P2), R11

  2230. 	ADCQ	(128)(REG_P2), R12

  2231. 	ADCQ	(136)(REG_P2), R13

  2232. 	ADCQ	(144)(REG_P2), R14

  2233. 	ADCQ	(152)(REG_P2), R15

  2234. 	ADCQ	(160)(REG_P2), AX

  2235. 	ADCQ	(168)(REG_P2), BX

  2236. 	ADCQ	(176)(REG_P2), CX

  2237. 	ADCQ	(184)(REG_P2), DI

  2238. 

  2239. 	MOVQ	R8, (96)(REG_P3)

  2240. 	MOVQ	R9, (104)(REG_P3)

  2241. 	MOVQ	R10, (112)(REG_P3)

  2242. 	MOVQ	R11, (120)(REG_P3)

  2243. 	MOVQ	R12, (128)(REG_P3)

  2244. 	MOVQ	R13, (136)(REG_P3)

  2245. 	MOVQ	R14, (144)(REG_P3)

  2246. 	MOVQ	R15, (152)(REG_P3)

  2247. 	MOVQ	AX, (160)(REG_P3)

  2248. 	MOVQ	BX, (168)(REG_P3)

  2249. 	MOVQ	CX, (176)(REG_P3)

  2250. 	MOVQ	DI, (184)(REG_P3)

  2251. 

  2252. 	RET

  2253. 

  2254. 

  2255. TEXT ·fp751X2SubLazy(SB), NOSPLIT, $0-24

  2256. 

  2257. 	MOVQ z+0(FP), REG_P3

  2258. 	MOVQ x+8(FP), REG_P1

  2259. 	MOVQ y+16(FP), REG_P2

  2260. 

  2261. 	MOVQ	(REG_P1), R8

  2262. 	MOVQ	(8)(REG_P1), R9

  2263. 	MOVQ	(16)(REG_P1), R10

  2264. 	MOVQ	(24)(REG_P1), R11

  2265. 	MOVQ	(32)(REG_P1), R12

  2266. 	MOVQ	(40)(REG_P1), R13

  2267. 	MOVQ	(48)(REG_P1), R14

  2268. 	MOVQ	(56)(REG_P1), R15

  2269. 	MOVQ	(64)(REG_P1), AX

  2270. 	MOVQ	(72)(REG_P1), BX

  2271. 	MOVQ	(80)(REG_P1), CX

  2272. 

  2273. 	SUBQ	(REG_P2), R8

  2274. 	SBBQ	(8)(REG_P2), R9

  2275. 	SBBQ	(16)(REG_P2), R10

  2276. 	SBBQ	(24)(REG_P2), R11

  2277. 	SBBQ	(32)(REG_P2), R12

  2278. 	SBBQ	(40)(REG_P2), R13

  2279. 	SBBQ	(48)(REG_P2), R14

  2280. 	SBBQ	(56)(REG_P2), R15

  2281. 	SBBQ	(64)(REG_P2), AX

  2282. 	SBBQ	(72)(REG_P2), BX

  2283. 	SBBQ	(80)(REG_P2), CX

  2284. 

  2285. 	MOVQ	R8, (REG_P3)

  2286. 	MOVQ	R9, (8)(REG_P3)

  2287. 	MOVQ	R10, (16)(REG_P3)

  2288. 	MOVQ	R11, (24)(REG_P3)

  2289. 	MOVQ	R12, (32)(REG_P3)

  2290. 	MOVQ	R13, (40)(REG_P3)

  2291. 	MOVQ	R14, (48)(REG_P3)

  2292. 	MOVQ	R15, (56)(REG_P3)

  2293. 	MOVQ	AX, (64)(REG_P3)

  2294. 	MOVQ	BX, (72)(REG_P3)

  2295. 	MOVQ	CX, (80)(REG_P3)

  2296. 	MOVQ	(88)(REG_P1), AX

  2297. 	SBBQ	(88)(REG_P2), AX

  2298. 	MOVQ	AX, (88)(REG_P3)

  2299. 

  2300. 	MOVQ	(96)(REG_P1), R8

  2301. 	MOVQ	(104)(REG_P1), R9

  2302. 	MOVQ	(112)(REG_P1), R10

  2303. 	MOVQ	(120)(REG_P1), R11

  2304. 	MOVQ	(128)(REG_P1), R12

  2305. 	MOVQ	(136)(REG_P1), R13

  2306. 	MOVQ	(144)(REG_P1), R14

  2307. 	MOVQ	(152)(REG_P1), R15

  2308. 	MOVQ	(160)(REG_P1), AX

  2309. 	MOVQ	(168)(REG_P1), BX

  2310. 	MOVQ	(176)(REG_P1), CX

  2311. 	MOVQ	(184)(REG_P1), DI

  2312. 

  2313. 	SBBQ	(96)(REG_P2), R8

  2314. 	SBBQ	(104)(REG_P2), R9

  2315. 	SBBQ	(112)(REG_P2), R10

  2316. 	SBBQ	(120)(REG_P2), R11

  2317. 	SBBQ	(128)(REG_P2), R12

  2318. 	SBBQ	(136)(REG_P2), R13

  2319. 	SBBQ	(144)(REG_P2), R14

  2320. 	SBBQ	(152)(REG_P2), R15

  2321. 	SBBQ	(160)(REG_P2), AX

  2322. 	SBBQ	(168)(REG_P2), BX

  2323. 	SBBQ	(176)(REG_P2), CX

  2324. 	SBBQ	(184)(REG_P2), DI

  2325. 

  2326. 	MOVQ	R8, (96)(REG_P3)

  2327. 	MOVQ	R9, (104)(REG_P3)

  2328. 	MOVQ	R10, (112)(REG_P3)

  2329. 	MOVQ	R11, (120)(REG_P3)

  2330. 	MOVQ	R12, (128)(REG_P3)

  2331. 	MOVQ	R13, (136)(REG_P3)

  2332. 	MOVQ	R14, (144)(REG_P3)

  2333. 	MOVQ	R15, (152)(REG_P3)

  2334. 	MOVQ	AX, (160)(REG_P3)

  2335. 	MOVQ	BX, (168)(REG_P3)

  2336. 	MOVQ	CX, (176)(REG_P3)

  2337. 	MOVQ	DI, (184)(REG_P3)

  2338. 

  2339. 	// Now the carry flag is 1 if x-y < 0.  If so, add p*2^768.

  2340. 	ZERO_AX_WITHOUT_CLOBBERING_FLAGS

  2341. 	SBBQ	$0, AX

  2342. 

  2343. 	// Load p into registers:

  2344. 	MOVQ	P751_0, R8

  2345. 	// P751_{1,2,3,4} = P751_0, so reuse R8

  2346. 	MOVQ	P751_5, R9

  2347. 	MOVQ	P751_6, R10

  2348. 	MOVQ	P751_7, R11

  2349. 	MOVQ	P751_8, R12

  2350. 	MOVQ	P751_9, R13

  2351. 	MOVQ	P751_10, R14

  2352. 	MOVQ	P751_11, R15

  2353. 

  2354. 	ANDQ	AX, R8

  2355. 	ANDQ	AX, R9

  2356. 	ANDQ	AX, R10

  2357. 	ANDQ	AX, R11

  2358. 	ANDQ	AX, R12

  2359. 	ANDQ	AX, R13

  2360. 	ANDQ	AX, R14

  2361. 	ANDQ	AX, R15

  2362. 

  2363. 	ADDQ	R8,  (96   )(REG_P3)

  2364. 	ADCQ	R8,  (96+ 8)(REG_P3)

  2365. 	ADCQ	R8,  (96+16)(REG_P3)

  2366. 	ADCQ	R8,  (96+24)(REG_P3)

  2367. 	ADCQ	R8,  (96+32)(REG_P3)

  2368. 	ADCQ	R9,  (96+40)(REG_P3)

  2369. 	ADCQ	R10, (96+48)(REG_P3)

  2370. 	ADCQ	R11, (96+56)(REG_P3)

  2371. 	ADCQ	R12, (96+64)(REG_P3)

  2372. 	ADCQ	R13, (96+72)(REG_P3)

  2373. 	ADCQ	R14, (96+80)(REG_P3)

  2374. 	ADCQ    R15, (96+88)(REG_P3)

  2375. 

  2376. 	RET