kris
/
SIDH_p751
1
0
Креирај огранак 0
Код Дискусије 0 Захтеви за спајање 0 Издања 0 Вики Activity
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.
135 Комити
14 Гране
653 KiB
 
 
 
Дрво: af904debd0
Гране Ознаке
${ item.name }
Create branch ${ searchTerm }
from 'af904debd0'
${ noResults }
SIDH_p751/p751/arith_amd64.s

2621 lines
45 KiB
Датотека Blame Историја 

  1. // +build amd64,!noasm

  2. 

  3. #include "textflag.h"

  4. 

  5. // p751 + 1

  6. #define P751P1_5   $0xEEB0000000000000

  7. #define P751P1_6   $0xE3EC968549F878A8

  8. #define P751P1_7   $0xDA959B1A13F7CC76

  9. #define P751P1_8   $0x084E9867D6EBE876

  10. #define P751P1_9   $0x8562B5045CB25748

  11. #define P751P1_10  $0x0E12909F97BADC66

  12. #define P751P1_11  $0x00006FE5D541F71C

  13. 

  14. #define P751_0     $0xFFFFFFFFFFFFFFFF

  15. #define P751_5     $0xEEAFFFFFFFFFFFFF

  16. #define P751_6     $0xE3EC968549F878A8

  17. #define P751_7     $0xDA959B1A13F7CC76

  18. #define P751_8     $0x084E9867D6EBE876

  19. #define P751_9     $0x8562B5045CB25748

  20. #define P751_10    $0x0E12909F97BADC66

  21. #define P751_11    $0x00006FE5D541F71C

  22. 

  23. #define P751X2_0   $0xFFFFFFFFFFFFFFFE

  24. #define P751X2_1   $0xFFFFFFFFFFFFFFFF

  25. #define P751X2_5   $0xDD5FFFFFFFFFFFFF

  26. #define P751X2_6   $0xC7D92D0A93F0F151

  27. #define P751X2_7   $0xB52B363427EF98ED

  28. #define P751X2_8   $0x109D30CFADD7D0ED

  29. #define P751X2_9   $0x0AC56A08B964AE90

  30. #define P751X2_10  $0x1C25213F2F75B8CD

  31. #define P751X2_11  $0x0000DFCBAA83EE38

  32. 

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

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

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

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

  37. 

  38. #define REG_P1 DI

  39. #define REG_P2 SI

  40. #define REG_P3 DX

  41. 

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

  43. 	MOVQ	x+0(FP), REG_P1

  44. 

  45. 	// Zero AX for later use:

  46. 	XORQ	AX, AX

  47. 

  48. 	// Load p into registers:

  49. 	MOVQ	P751_0, R8

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

  51. 	MOVQ	P751_5, R9

  52. 	MOVQ	P751_6, R10

  53. 	MOVQ	P751_7, R11

  54. 	MOVQ	P751_8, R12

  55. 	MOVQ	P751_9, R13

  56. 	MOVQ	P751_10, R14

  57. 	MOVQ	P751_11, R15

  58. 

  59. 	// Set x <- x - p

  60. 	SUBQ	R8, (REG_P1)

  61. 	SBBQ	R8, (8)(REG_P1)

  62. 	SBBQ	R8, (16)(REG_P1)

  63. 	SBBQ	R8, (24)(REG_P1)

  64. 	SBBQ	R8, (32)(REG_P1)

  65. 	SBBQ	R9, (40)(REG_P1)

  66. 	SBBQ	R10, (48)(REG_P1)

  67. 	SBBQ	R11, (56)(REG_P1)

  68. 	SBBQ	R12, (64)(REG_P1)

  69. 	SBBQ	R13, (72)(REG_P1)

  70. 	SBBQ	R14, (80)(REG_P1)

  71. 	SBBQ    R15, (88)(REG_P1)

  72. 

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

  74. 	SBBQ	$0, AX

  75. 

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

  77. 	ANDQ	AX, R8

  78. 	ANDQ	AX, R9

  79. 	ANDQ	AX, R10

  80. 	ANDQ	AX, R11

  81. 	ANDQ	AX, R12

  82. 	ANDQ	AX, R13

  83. 	ANDQ	AX, R14

  84. 	ANDQ	AX, R15

  85. 

  86. 	ADDQ	R8, (REG_P1)

  87. 	ADCQ	R8, (8)(REG_P1)

  88. 	ADCQ	R8, (16)(REG_P1)

  89. 	ADCQ	R8, (24)(REG_P1)

  90. 	ADCQ	R8, (32)(REG_P1)

  91. 	ADCQ	R9, (40)(REG_P1)

  92. 	ADCQ	R10, (48)(REG_P1)

  93. 	ADCQ	R11, (56)(REG_P1)

  94. 	ADCQ	R12, (64)(REG_P1)

  95. 	ADCQ	R13, (72)(REG_P1)

  96. 	ADCQ	R14, (80)(REG_P1)

  97. 	ADCQ    R15, (88)(REG_P1)

  98. 

  99. 	RET

  100. 

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

  102. 

  103. 	MOVQ	x+0(FP), REG_P1

  104. 	MOVQ	y+8(FP), REG_P2

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

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

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

  108. 

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

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

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

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

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

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

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

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

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

  118. 

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

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

  121. 	MOVQ	CX, DX

  122. 	XORQ	BX, DX

  123. 	ANDQ	AX, DX

  124. 	XORQ	DX, BX

  125. 	XORQ	DX, CX

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

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

  128. 

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

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

  131. 	MOVQ	CX, DX

  132. 	XORQ	BX, DX

  133. 	ANDQ	AX, DX

  134. 	XORQ	DX, BX

  135. 	XORQ	DX, CX

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

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

  138. 

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

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

  141. 	MOVQ	CX, DX

  142. 	XORQ	BX, DX

  143. 	ANDQ	AX, DX

  144. 	XORQ	DX, BX

  145. 	XORQ	DX, CX

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

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

  148. 

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

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

  151. 	MOVQ	CX, DX

  152. 	XORQ	BX, DX

  153. 	ANDQ	AX, DX

  154. 	XORQ	DX, BX

  155. 	XORQ	DX, CX

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

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

  158. 

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

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

  161. 	MOVQ	CX, DX

  162. 	XORQ	BX, DX

  163. 	ANDQ	AX, DX

  164. 	XORQ	DX, BX

  165. 	XORQ	DX, CX

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

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

  168. 

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

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

  171. 	MOVQ	CX, DX

  172. 	XORQ	BX, DX

  173. 	ANDQ	AX, DX

  174. 	XORQ	DX, BX

  175. 	XORQ	DX, CX

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

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

  178. 

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

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

  181. 	MOVQ	CX, DX

  182. 	XORQ	BX, DX

  183. 	ANDQ	AX, DX

  184. 	XORQ	DX, BX

  185. 	XORQ	DX, CX

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

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

  188. 

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

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

  191. 	MOVQ	CX, DX

  192. 	XORQ	BX, DX

  193. 	ANDQ	AX, DX

  194. 	XORQ	DX, BX

  195. 	XORQ	DX, CX

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

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

  198. 

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

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

  201. 	MOVQ	CX, DX

  202. 	XORQ	BX, DX

  203. 	ANDQ	AX, DX

  204. 	XORQ	DX, BX

  205. 	XORQ	DX, CX

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

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

  208. 

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

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

  211. 	MOVQ	CX, DX

  212. 	XORQ	BX, DX

  213. 	ANDQ	AX, DX

  214. 	XORQ	DX, BX

  215. 	XORQ	DX, CX

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

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

  218. 

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

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

  221. 	MOVQ	CX, DX

  222. 	XORQ	BX, DX

  223. 	ANDQ	AX, DX

  224. 	XORQ	DX, BX

  225. 	XORQ	DX, CX

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

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

  228. 

  229. 	RET

  230. 

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

  232. 

  233. 	MOVQ	z+0(FP), REG_P3

  234. 	MOVQ	x+8(FP), REG_P1

  235. 	MOVQ	y+16(FP), REG_P2

  236. 

  237. 	MOVQ	(REG_P1), R8

  238. 	MOVQ	(8)(REG_P1), R9

  239. 	MOVQ	(16)(REG_P1), R10

  240. 	MOVQ	(24)(REG_P1), R11

  241. 	MOVQ	(32)(REG_P1), R12

  242. 	MOVQ	(40)(REG_P1), R13

  243. 	MOVQ	(48)(REG_P1), R14

  244. 	MOVQ	(56)(REG_P1), R15

  245. 	MOVQ	(64)(REG_P1), CX

  246. 	ADDQ	(REG_P2), R8

  247. 	ADCQ	(8)(REG_P2), R9

  248. 	ADCQ	(16)(REG_P2), R10

  249. 	ADCQ	(24)(REG_P2), R11

  250. 	ADCQ	(32)(REG_P2), R12

  251. 	ADCQ	(40)(REG_P2), R13

  252. 	ADCQ	(48)(REG_P2), R14

  253. 	ADCQ	(56)(REG_P2), R15

  254. 	ADCQ	(64)(REG_P2), CX

  255. 	MOVQ	(72)(REG_P1), AX

  256. 	ADCQ	(72)(REG_P2), AX

  257. 	MOVQ	AX, (72)(REG_P3)

  258. 	MOVQ	(80)(REG_P1), AX

  259. 	ADCQ	(80)(REG_P2), AX

  260. 	MOVQ	AX, (80)(REG_P3)

  261. 	MOVQ	(88)(REG_P1), AX

  262. 	ADCQ	(88)(REG_P2), AX

  263. 	MOVQ	AX, (88)(REG_P3)

  264. 

  265. 	MOVQ	P751X2_0, AX

  266. 	SUBQ	AX, R8

  267. 	MOVQ	P751X2_1, AX

  268. 	SBBQ	AX, R9

  269. 	SBBQ	AX, R10

  270. 	SBBQ	AX, R11

  271. 	SBBQ	AX, R12

  272. 	MOVQ	P751X2_5, AX

  273. 	SBBQ	AX, R13

  274. 	MOVQ	P751X2_6, AX

  275. 	SBBQ	AX, R14

  276. 	MOVQ	P751X2_7, AX

  277. 	SBBQ	AX, R15

  278. 	MOVQ	P751X2_8, AX

  279. 	SBBQ	AX, CX

  280. 	MOVQ	R8, (REG_P3)

  281. 	MOVQ	R9, (8)(REG_P3)

  282. 	MOVQ	R10, (16)(REG_P3)

  283. 	MOVQ	R11, (24)(REG_P3)

  284. 	MOVQ	R12, (32)(REG_P3)

  285. 	MOVQ	R13, (40)(REG_P3)

  286. 	MOVQ	R14, (48)(REG_P3)

  287. 	MOVQ	R15, (56)(REG_P3)

  288. 	MOVQ	CX, (64)(REG_P3)

  289. 	MOVQ	(72)(REG_P3), R8

  290. 	MOVQ	(80)(REG_P3), R9

  291. 	MOVQ	(88)(REG_P3), R10

  292. 	MOVQ	P751X2_9, AX

  293. 	SBBQ	AX, R8

  294. 	MOVQ	P751X2_10, AX

  295. 	SBBQ	AX, R9

  296. 	MOVQ	P751X2_11, AX

  297. 	SBBQ	AX, R10

  298. 	MOVQ	R8, (72)(REG_P3)

  299. 	MOVQ	R9, (80)(REG_P3)

  300. 	MOVQ	R10, (88)(REG_P3)

  301. 	MOVQ	$0, AX

  302. 	SBBQ	$0, AX

  303. 

  304. 	MOVQ	P751X2_0, SI

  305. 	ANDQ	AX, SI

  306. 	MOVQ	P751X2_1, R8

  307. 	ANDQ	AX, R8

  308. 	MOVQ	P751X2_5, R9

  309. 	ANDQ	AX, R9

  310. 	MOVQ	P751X2_6, R10

  311. 	ANDQ	AX, R10

  312. 	MOVQ	P751X2_7, R11

  313. 	ANDQ	AX, R11

  314. 	MOVQ	P751X2_8, R12

  315. 	ANDQ	AX, R12

  316. 	MOVQ	P751X2_9, R13

  317. 	ANDQ	AX, R13

  318. 	MOVQ	P751X2_10, R14

  319. 	ANDQ	AX, R14

  320. 	MOVQ	P751X2_11, R15

  321. 	ANDQ	AX, R15

  322. 

  323. 	MOVQ	(REG_P3), AX

  324. 	ADDQ	SI, AX

  325. 	MOVQ	AX, (REG_P3)

  326. 	MOVQ	(8)(REG_P3), AX

  327. 	ADCQ	R8, AX

  328. 	MOVQ	AX, (8)(REG_P3)

  329. 	MOVQ	(16)(REG_P3), AX

  330. 	ADCQ	R8, AX

  331. 	MOVQ	AX, (16)(REG_P3)

  332. 	MOVQ	(24)(REG_P3), AX

  333. 	ADCQ	R8, AX

  334. 	MOVQ	AX, (24)(REG_P3)

  335. 	MOVQ	(32)(REG_P3), AX

  336. 	ADCQ	R8, AX

  337. 	MOVQ	AX, (32)(REG_P3)

  338. 	MOVQ	(40)(REG_P3), AX

  339. 	ADCQ	R9, AX

  340. 	MOVQ	AX, (40)(REG_P3)

  341. 	MOVQ	(48)(REG_P3), AX

  342. 	ADCQ	R10, AX

  343. 	MOVQ	AX, (48)(REG_P3)

  344. 	MOVQ	(56)(REG_P3), AX

  345. 	ADCQ	R11, AX

  346. 	MOVQ	AX, (56)(REG_P3)

  347. 	MOVQ	(64)(REG_P3), AX

  348. 	ADCQ	R12, AX

  349. 	MOVQ	AX, (64)(REG_P3)

  350. 	MOVQ	(72)(REG_P3), AX

  351. 	ADCQ	R13, AX

  352. 	MOVQ	AX, (72)(REG_P3)

  353. 	MOVQ	(80)(REG_P3), AX

  354. 	ADCQ	R14, AX

  355. 	MOVQ	AX, (80)(REG_P3)

  356. 	MOVQ	(88)(REG_P3), AX

  357. 	ADCQ	R15, AX

  358. 	MOVQ	AX, (88)(REG_P3)

  359. 

  360. 	RET

  361. 

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

  363. 

  364. 	MOVQ	z+0(FP),  REG_P3

  365. 	MOVQ	x+8(FP),  REG_P1

  366. 	MOVQ	y+16(FP),  REG_P2

  367. 

  368. 	MOVQ	(REG_P1), R8

  369. 	MOVQ	(8)(REG_P1), R9

  370. 	MOVQ	(16)(REG_P1), R10

  371. 	MOVQ	(24)(REG_P1), R11

  372. 	MOVQ	(32)(REG_P1), R12

  373. 	MOVQ	(40)(REG_P1), R13

  374. 	MOVQ	(48)(REG_P1), R14

  375. 	MOVQ	(56)(REG_P1), R15

  376. 	MOVQ	(64)(REG_P1), CX

  377. 	SUBQ	(REG_P2), R8

  378. 	SBBQ	(8)(REG_P2), R9

  379. 	SBBQ	(16)(REG_P2), R10

  380. 	SBBQ	(24)(REG_P2), R11

  381. 	SBBQ	(32)(REG_P2), R12

  382. 	SBBQ	(40)(REG_P2), R13

  383. 	SBBQ	(48)(REG_P2), R14

  384. 	SBBQ	(56)(REG_P2), R15

  385. 	SBBQ	(64)(REG_P2), CX

  386. 	MOVQ	R8, (REG_P3)

  387. 	MOVQ	R9, (8)(REG_P3)

  388. 	MOVQ	R10, (16)(REG_P3)

  389. 	MOVQ	R11, (24)(REG_P3)

  390. 	MOVQ	R12, (32)(REG_P3)

  391. 	MOVQ	R13, (40)(REG_P3)

  392. 	MOVQ	R14, (48)(REG_P3)

  393. 	MOVQ	R15, (56)(REG_P3)

  394. 	MOVQ	CX, (64)(REG_P3)

  395. 	MOVQ	(72)(REG_P1), AX

  396. 	SBBQ	(72)(REG_P2), AX

  397. 	MOVQ	AX, (72)(REG_P3)

  398. 	MOVQ	(80)(REG_P1), AX

  399. 	SBBQ	(80)(REG_P2), AX

  400. 	MOVQ	AX, (80)(REG_P3)

  401. 	MOVQ	(88)(REG_P1), AX

  402. 	SBBQ	(88)(REG_P2), AX

  403. 	MOVQ	AX, (88)(REG_P3)

  404. 	MOVQ	$0, AX

  405. 	SBBQ	$0, AX

  406. 

  407. 	MOVQ	P751X2_0, SI

  408. 	ANDQ	AX, SI

  409. 	MOVQ	P751X2_1, R8

  410. 	ANDQ	AX, R8

  411. 	MOVQ	P751X2_5, R9

  412. 	ANDQ	AX, R9

  413. 	MOVQ	P751X2_6, R10

  414. 	ANDQ	AX, R10

  415. 	MOVQ	P751X2_7, R11

  416. 	ANDQ	AX, R11

  417. 	MOVQ	P751X2_8, R12

  418. 	ANDQ	AX, R12

  419. 	MOVQ	P751X2_9, R13

  420. 	ANDQ	AX, R13

  421. 	MOVQ	P751X2_10, R14

  422. 	ANDQ	AX, R14

  423. 	MOVQ	P751X2_11, R15

  424. 	ANDQ	AX, R15

  425. 

  426. 	MOVQ	(REG_P3), AX

  427. 	ADDQ	SI, AX

  428. 	MOVQ	AX, (REG_P3)

  429. 	MOVQ	(8)(REG_P3), AX

  430. 	ADCQ	R8, AX

  431. 	MOVQ	AX, (8)(REG_P3)

  432. 	MOVQ	(16)(REG_P3), AX

  433. 	ADCQ	R8, AX

  434. 	MOVQ	AX, (16)(REG_P3)

  435. 	MOVQ	(24)(REG_P3), AX

  436. 	ADCQ	R8, AX

  437. 	MOVQ	AX, (24)(REG_P3)

  438. 	MOVQ	(32)(REG_P3), AX

  439. 	ADCQ	R8, AX

  440. 	MOVQ	AX, (32)(REG_P3)

  441. 	MOVQ	(40)(REG_P3), AX

  442. 	ADCQ	R9, AX

  443. 	MOVQ	AX, (40)(REG_P3)

  444. 	MOVQ	(48)(REG_P3), AX

  445. 	ADCQ	R10, AX

  446. 	MOVQ	AX, (48)(REG_P3)

  447. 	MOVQ	(56)(REG_P3), AX

  448. 	ADCQ	R11, AX

  449. 	MOVQ	AX, (56)(REG_P3)

  450. 	MOVQ	(64)(REG_P3), AX

  451. 	ADCQ	R12, AX

  452. 	MOVQ	AX, (64)(REG_P3)

  453. 	MOVQ	(72)(REG_P3), AX

  454. 	ADCQ	R13, AX

  455. 	MOVQ	AX, (72)(REG_P3)

  456. 	MOVQ	(80)(REG_P3), AX

  457. 	ADCQ	R14, AX

  458. 	MOVQ	AX, (80)(REG_P3)

  459. 	MOVQ	(88)(REG_P3), AX

  460. 	ADCQ	R15, AX

  461. 	MOVQ	AX, (88)(REG_P3)

  462. 

  463. 	RET

  464. 

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

  466. 

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

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

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

  470. 

  471. 	MOVQ	z+0(FP), CX

  472. 	MOVQ	x+8(FP), REG_P1

  473. 	MOVQ	y+16(FP), REG_P2

  474. 

  475. 	XORQ	AX, AX

  476. 	MOVQ	(48)(REG_P1), R8

  477. 	MOVQ	(56)(REG_P1), R9

  478. 	MOVQ	(64)(REG_P1), R10

  479. 	MOVQ	(72)(REG_P1), R11

  480. 	MOVQ	(80)(REG_P1), R12

  481. 	MOVQ	(88)(REG_P1), R13

  482. 	ADDQ	(REG_P1), R8

  483. 	ADCQ	(8)(REG_P1), R9

  484. 	ADCQ	(16)(REG_P1), R10

  485. 	ADCQ	(24)(REG_P1), R11

  486. 	ADCQ	(32)(REG_P1), R12

  487. 	ADCQ	(40)(REG_P1), R13

  488. 	MOVQ	R8, (CX)

  489. 	MOVQ	R9, (8)(CX)

  490. 	MOVQ	R10, (16)(CX)

  491. 	MOVQ	R11, (24)(CX)

  492. 	MOVQ	R12, (32)(CX)

  493. 	MOVQ	R13, (40)(CX)

  494. 	SBBQ	$0, AX

  495. 

  496. 	XORQ	DX, DX

  497. 	MOVQ	(48)(REG_P2), R8

  498. 	MOVQ	(56)(REG_P2), R9

  499. 	MOVQ	(64)(REG_P2), R10

  500. 	MOVQ	(72)(REG_P2), R11

  501. 	MOVQ	(80)(REG_P2), R12

  502. 	MOVQ	(88)(REG_P2), R13

  503. 	ADDQ	(REG_P2), R8

  504. 	ADCQ	(8)(REG_P2), R9

  505. 	ADCQ	(16)(REG_P2), R10

  506. 	ADCQ	(24)(REG_P2), R11

  507. 	ADCQ	(32)(REG_P2), R12

  508. 	ADCQ	(40)(REG_P2), R13

  509. 	MOVQ	R8, (48)(CX)

  510. 	MOVQ	R9, (56)(CX)

  511. 	MOVQ	R10, (64)(CX)

  512. 	MOVQ	R11, (72)(CX)

  513. 	MOVQ	R12, (80)(CX)

  514. 	MOVQ	R13, (88)(CX)

  515. 	SBBQ	$0, DX

  516. 	MOVQ	AX, (80)(SP)

  517. 	MOVQ	DX, (88)(SP)

  518. 

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

  520. 

  521. 	MOVQ	(CX), R11

  522. 	MOVQ	R8, AX

  523. 	MULQ	R11

  524. 	MOVQ	AX, (SP)		// c0

  525. 	MOVQ	DX, R14

  526. 

  527. 	XORQ	R15, R15

  528. 	MOVQ	R9, AX

  529. 	MULQ	R11

  530. 	XORQ	R9, R9

  531. 	ADDQ	AX, R14

  532. 	ADCQ	DX, R9

  533. 

  534. 	MOVQ	(8)(CX), R12

  535. 	MOVQ	R8, AX

  536. 	MULQ	R12

  537. 	ADDQ	AX, R14

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

  539. 	ADCQ	DX, R9

  540. 	ADCQ	$0, R15

  541. 

  542. 	XORQ	R8, R8

  543. 	MOVQ	R10, AX

  544. 	MULQ	R11

  545. 	ADDQ	AX, R9

  546. 	MOVQ	(48)(CX), R13

  547. 	ADCQ	DX, R15

  548. 	ADCQ	$0, R8

  549. 

  550. 	MOVQ	(16)(CX), AX

  551. 	MULQ	R13

  552. 	ADDQ	AX, R9

  553. 	ADCQ	DX, R15

  554. 	MOVQ	(56)(CX), AX

  555. 	ADCQ	$0, R8

  556. 

  557. 	MULQ	R12

  558. 	ADDQ	AX, R9

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

  560. 	ADCQ	DX, R15

  561. 	ADCQ	$0, R8

  562. 

  563. 	XORQ	R9, R9

  564. 	MOVQ	(72)(CX), AX

  565. 	MULQ	R11

  566. 	ADDQ	AX, R15

  567. 	ADCQ	DX, R8

  568. 	ADCQ	$0, R9

  569. 

  570. 	MOVQ	(24)(CX), AX

  571. 	MULQ	R13

  572. 	ADDQ	AX, R15

  573. 	ADCQ	DX, R8

  574. 	ADCQ	$0, R9

  575. 

  576. 	MOVQ	R10, AX

  577. 	MULQ	R12

  578. 	ADDQ	AX, R15

  579. 	ADCQ	DX, R8

  580. 	ADCQ	$0, R9

  581. 

  582. 	MOVQ	(16)(CX), R14

  583. 	MOVQ	(56)(CX), AX

  584. 	MULQ	R14

  585. 	ADDQ	AX, R15

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

  587. 	ADCQ	DX, R8

  588. 	ADCQ	$0, R9

  589. 

  590. 	XORQ	R10, R10

  591. 	MOVQ	(80)(CX), AX

  592. 	MULQ	R11

  593. 	ADDQ	AX, R8

  594. 	ADCQ	DX, R9

  595. 	ADCQ	$0, R10

  596. 

  597. 	MOVQ	(64)(CX), AX

  598. 	MULQ	R14

  599. 	ADDQ	AX, R8

  600. 	ADCQ	DX, R9

  601. 	ADCQ	$0, R10

  602. 

  603. 	MOVQ	(48)(CX), R15

  604. 	MOVQ	(32)(CX), AX

  605. 	MULQ	R15

  606. 	ADDQ	AX, R8

  607. 	ADCQ	DX, R9

  608. 	ADCQ	$0, R10

  609. 

  610. 	MOVQ	(72)(CX), AX

  611. 	MULQ	R12

  612. 	ADDQ	AX, R8

  613. 	ADCQ	DX, R9

  614. 	ADCQ	$0, R10

  615. 

  616. 	MOVQ	(24)(CX), R13

  617. 	MOVQ	(56)(CX), AX

  618. 	MULQ	R13

  619. 	ADDQ	AX, R8

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

  621. 	ADCQ	DX, R9

  622. 	ADCQ	$0, R10

  623. 

  624. 	XORQ	R8, R8

  625. 	MOVQ	(88)(CX), AX

  626. 	MULQ	R11

  627. 	ADDQ	AX, R9

  628. 	ADCQ	DX, R10

  629. 	ADCQ	$0, R8

  630. 

  631. 	MOVQ	(64)(CX), AX

  632. 	MULQ	R13

  633. 	ADDQ	AX, R9

  634. 	ADCQ	DX, R10

  635. 	ADCQ	$0, R8

  636. 

  637. 	MOVQ	(72)(CX), AX

  638. 	MULQ	R14

  639. 	ADDQ	AX, R9

  640. 	ADCQ	DX, R10

  641. 	ADCQ	$0, R8

  642. 

  643. 	MOVQ	(40)(CX), AX

  644. 	MULQ	R15

  645. 	ADDQ	AX, R9

  646. 	ADCQ	DX, R10

  647. 	ADCQ	$0, R8

  648. 

  649. 	MOVQ	(80)(CX), AX

  650. 	MULQ	R12

  651. 	ADDQ	AX, R9

  652. 	ADCQ	DX, R10

  653. 	ADCQ	$0, R8

  654. 

  655. 	MOVQ	(32)(CX), R15

  656. 	MOVQ	(56)(CX), AX

  657. 	MULQ	R15

  658. 	ADDQ	AX, R9

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

  660. 	ADCQ	DX, R10

  661. 	ADCQ	$0, R8

  662. 

  663. 	XORQ	R9, R9

  664. 	MOVQ	(64)(CX), AX

  665. 	MULQ	R15

  666. 	ADDQ	AX, R10

  667. 	ADCQ	DX, R8

  668. 	ADCQ	$0, R9

  669. 

  670. 	MOVQ	(88)(CX), AX

  671. 	MULQ	R12

  672. 	ADDQ	AX, R10

  673. 	ADCQ	DX, R8

  674. 	ADCQ	$0, R9

  675. 

  676. 	MOVQ	(80)(CX), AX

  677. 	MULQ	R14

  678. 	ADDQ	AX, R10

  679. 	ADCQ	DX, R8

  680. 	ADCQ	$0, R9

  681. 

  682. 	MOVQ	(40)(CX), R11

  683. 	MOVQ	(56)(CX), AX

  684. 	MULQ	R11

  685. 	ADDQ	AX, R10

  686. 	ADCQ	DX, R8

  687. 	ADCQ	$0, R9

  688. 

  689. 	MOVQ	(72)(CX), AX

  690. 	MULQ	R13

  691. 	ADDQ	AX, R10

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

  693. 	ADCQ	DX, R8

  694. 	ADCQ	$0, R9

  695. 

  696. 	XORQ	R10, R10

  697. 	MOVQ	(88)(CX), AX

  698. 	MULQ	R14

  699. 	ADDQ	AX, R8

  700. 	ADCQ	DX, R9

  701. 	ADCQ	$0, R10

  702. 

  703. 	MOVQ	(64)(CX), AX

  704. 	MULQ	R11

  705. 	ADDQ	AX, R8

  706. 	ADCQ	DX, R9

  707. 	ADCQ	$0, R10

  708. 

  709. 	MOVQ	(80)(CX), AX

  710. 	MULQ	R13

  711. 	ADDQ	AX, R8

  712. 	ADCQ	DX, R9

  713. 	ADCQ	$0, R10

  714. 

  715. 	MOVQ	(72)(CX), AX

  716. 	MULQ	R15

  717. 	ADDQ	AX, R8

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

  719. 	ADCQ	DX, R9

  720. 	ADCQ	$0, R10

  721. 

  722. 	XORQ	R8, R8

  723. 	MOVQ	(72)(CX), AX

  724. 	MULQ	R11

  725. 	ADDQ	AX, R9

  726. 	ADCQ	DX, R10

  727. 	ADCQ	$0, R8

  728. 

  729. 	MOVQ	(80)(CX), AX

  730. 	MULQ	R15

  731. 	ADDQ	AX, R9

  732. 	ADCQ	DX, R10

  733. 	ADCQ	$0, R8

  734. 

  735. 	MOVQ	(88)(CX), AX

  736. 	MULQ	R13

  737. 	ADDQ	AX, R9

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

  739. 	ADCQ	DX, R10

  740. 	ADCQ	$0, R8

  741. 

  742. 	XORQ	R9, R9

  743. 	MOVQ	(88)(CX), AX

  744. 	MULQ	R15

  745. 	ADDQ	AX, R10

  746. 	ADCQ	DX, R8

  747. 	ADCQ	$0, R9

  748. 

  749. 	MOVQ	(80)(CX), AX

  750. 	MULQ	R11

  751. 	ADDQ	AX, R10			// c9

  752. 	ADCQ	DX, R8

  753. 	ADCQ	$0, R9

  754. 

  755. 	MOVQ	(88)(CX), AX

  756. 	MULQ	R11

  757. 	ADDQ	AX, R8			// c10

  758. 	ADCQ	DX, R9			// c11

  759. 

  760. 	MOVQ	(88)(SP), AX

  761. 	MOVQ	(CX), DX

  762. 	ANDQ	AX, R12

  763. 	ANDQ	AX, R14

  764. 	ANDQ	AX, DX

  765. 	ANDQ	AX, R13

  766. 	ANDQ	AX, R15

  767. 	ANDQ	AX, R11

  768. 	MOVQ	(48)(SP), AX

  769. 	ADDQ	AX, DX

  770. 	MOVQ	(56)(SP), AX

  771. 	ADCQ	AX, R12

  772. 	MOVQ	(64)(SP), AX

  773. 	ADCQ	AX, R14

  774. 	ADCQ	R10, R13

  775. 	ADCQ	R8, R15

  776. 	ADCQ	R9, R11

  777. 	MOVQ	(80)(SP), AX

  778. 	MOVQ	DX, (48)(SP)

  779. 	MOVQ	R12, (56)(SP)

  780. 	MOVQ	R14, (64)(SP)

  781. 	MOVQ	R13, (72)(SP)

  782. 	MOVQ	R15, (80)(SP)

  783. 	MOVQ	R11, (88)(SP)

  784. 

  785. 	MOVQ	(48)(CX), R8

  786. 	MOVQ	(56)(CX), R9

  787. 	MOVQ	(64)(CX), R10

  788. 	MOVQ	(72)(CX), R11

  789. 	MOVQ	(80)(CX), R12

  790. 	MOVQ	(88)(CX), R13

  791. 	ANDQ	AX, R8

  792. 	ANDQ	AX, R9

  793. 	ANDQ	AX, R10

  794. 	ANDQ	AX, R11

  795. 	ANDQ	AX, R12

  796. 	ANDQ	AX, R13

  797. 	MOVQ	(48)(SP), AX

  798. 	ADDQ	AX, R8

  799. 	MOVQ	(56)(SP), AX

  800. 	ADCQ	AX, R9

  801. 	MOVQ	(64)(SP), AX

  802. 	ADCQ	AX, R10

  803. 	MOVQ	(72)(SP), AX

  804. 	ADCQ	AX, R11

  805. 	MOVQ	(80)(SP), AX

  806. 	ADCQ	AX, R12

  807. 	MOVQ	(88)(SP), AX

  808. 	ADCQ	AX, R13

  809. 	MOVQ	R8, (48)(SP)

  810. 	MOVQ	R9, (56)(SP)

  811. 	MOVQ	R11, (72)(SP)

  812. 

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

  814. 	MOVQ	(REG_P1), R11

  815. 	MOVQ	(REG_P2), AX

  816. 	MULQ	R11

  817. 	XORQ	R9, R9

  818. 	MOVQ	AX, (CX)		// c0

  819. 	MOVQ	R10, (64)(SP)

  820. 	MOVQ	DX, R8

  821. 

  822. 	MOVQ	(8)(REG_P2), AX

  823. 	MULQ	R11

  824. 	XORQ	R10, R10

  825. 	ADDQ	AX, R8

  826. 	MOVQ	R12, (80)(SP)

  827. 	ADCQ	DX, R9

  828. 

  829. 	MOVQ	(8)(REG_P1), R12

  830. 	MOVQ	(REG_P2), AX

  831. 	MULQ	R12

  832. 	ADDQ	AX, R8

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

  834. 	ADCQ	DX, R9

  835. 	MOVQ	R13, (88)(SP)

  836. 	ADCQ	$0, R10

  837. 

  838. 	XORQ	R8, R8

  839. 	MOVQ	(16)(REG_P2), AX

  840. 	MULQ	R11

  841. 	ADDQ	AX, R9

  842. 	ADCQ	DX, R10

  843. 	ADCQ	$0, R8

  844. 

  845. 	MOVQ	(REG_P2), R13

  846. 	MOVQ	(16)(REG_P1), AX

  847. 	MULQ	R13

  848. 	ADDQ	AX, R9

  849. 	ADCQ	DX, R10

  850. 	ADCQ	$0, R8

  851. 

  852. 	MOVQ	(8)(REG_P2), AX

  853. 	MULQ	R12

  854. 	ADDQ	AX, R9

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

  856. 	ADCQ	DX, R10

  857. 	ADCQ	$0, R8

  858. 

  859. 	XORQ	R9, R9

  860. 	MOVQ	(24)(REG_P2), AX

  861. 	MULQ	R11

  862. 	ADDQ	AX, R10

  863. 	ADCQ	DX, R8

  864. 	ADCQ	$0, R9

  865. 

  866. 	MOVQ	(24)(REG_P1), AX

  867. 	MULQ	R13

  868. 	ADDQ	AX, R10

  869. 	ADCQ	DX, R8

  870. 	ADCQ	$0, R9

  871. 

  872. 	MOVQ	(16)(REG_P2), AX

  873. 	MULQ	R12

  874. 	ADDQ	AX, R10

  875. 	ADCQ	DX, R8

  876. 	ADCQ	$0, R9

  877. 

  878. 	MOVQ	(16)(REG_P1), R14

  879. 	MOVQ	(8)(REG_P2), AX

  880. 	MULQ	R14

  881. 	ADDQ	AX, R10

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

  883. 	ADCQ	DX, R8

  884. 	ADCQ	$0, R9

  885. 

  886. 	XORQ	R10, R10

  887. 	MOVQ	(32)(REG_P2), AX

  888. 	MULQ	R11

  889. 	ADDQ	AX, R8

  890. 	ADCQ	DX, R9

  891. 	ADCQ	$0, R10

  892. 

  893. 	MOVQ	(16)(REG_P2), AX

  894. 	MULQ	R14

  895. 	ADDQ	AX, R8

  896. 	ADCQ	DX, R9

  897. 	ADCQ	$0, R10

  898. 

  899. 	MOVQ	(32)(REG_P1), AX

  900. 	MULQ	R13

  901. 	ADDQ	AX, R8

  902. 	ADCQ	DX, R9

  903. 	ADCQ	$0, R10

  904. 

  905. 	MOVQ	(24)(REG_P2), AX

  906. 	MULQ	R12

  907. 	ADDQ	AX, R8

  908. 	ADCQ	DX, R9

  909. 	ADCQ	$0, R10

  910. 

  911. 	MOVQ	(24)(REG_P1), R13

  912. 	MOVQ	(8)(REG_P2), AX

  913. 	MULQ	R13

  914. 	ADDQ	AX, R8

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

  916. 	ADCQ	DX, R9

  917. 	ADCQ	$0, R10

  918. 

  919. 	XORQ	R8, R8

  920. 	MOVQ	(40)(REG_P2), AX

  921. 	MULQ	R11

  922. 	ADDQ	AX, R9

  923. 	ADCQ	DX, R10

  924. 	ADCQ	$0, R8

  925. 

  926. 	MOVQ	(16)(REG_P2), AX

  927. 	MULQ	R13

  928. 	ADDQ	AX, R9

  929. 	ADCQ	DX, R10

  930. 	ADCQ	$0, R8

  931. 

  932. 	MOVQ	(24)(REG_P2), AX

  933. 	MULQ	R14

  934. 	ADDQ	AX, R9

  935. 	ADCQ	DX, R10

  936. 	ADCQ	$0, R8

  937. 

  938. 	MOVQ	(40)(REG_P1), R11

  939. 	MOVQ	(REG_P2), AX

  940. 	MULQ	R11

  941. 	ADDQ	AX, R9

  942. 	ADCQ	DX, R10

  943. 	ADCQ	$0, R8

  944. 

  945. 	MOVQ	(32)(REG_P2), AX

  946. 	MULQ	R12

  947. 	ADDQ	AX, R9

  948. 	ADCQ	DX, R10

  949. 	ADCQ	$0, R8

  950. 

  951. 	MOVQ	(32)(REG_P1), R15

  952. 	MOVQ	(8)(REG_P2), AX

  953. 	MULQ	R15

  954. 	ADDQ	AX, R9

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

  956. 	ADCQ	DX, R10

  957. 	ADCQ	$0, R8

  958. 

  959. 	XORQ	R9, R9

  960. 	MOVQ	(16)(REG_P2), AX

  961. 	MULQ	R15

  962. 	ADDQ	AX, R10

  963. 	ADCQ	DX, R8

  964. 	ADCQ	$0, R9

  965. 

  966. 	MOVQ	(40)(REG_P2), AX

  967. 	MULQ	R12

  968. 	ADDQ	AX, R10

  969. 	ADCQ	DX, R8

  970. 	ADCQ	$0, R9

  971. 

  972. 	MOVQ	(32)(REG_P2), AX

  973. 	MULQ	R14

  974. 	ADDQ	AX, R10

  975. 	ADCQ	DX, R8

  976. 	ADCQ	$0, R9

  977. 

  978. 	MOVQ	(8)(REG_P2), AX

  979. 	MULQ	R11

  980. 	ADDQ	AX, R10

  981. 	ADCQ	DX, R8

  982. 	ADCQ	$0, R9

  983. 

  984. 	MOVQ	(24)(REG_P2), AX

  985. 	MULQ	R13

  986. 	ADDQ	AX, R10

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

  988. 	ADCQ	DX, R8

  989. 	ADCQ	$0, R9

  990. 

  991. 	XORQ	R10, R10

  992. 	MOVQ	(40)(REG_P2), AX

  993. 	MULQ	R14

  994. 	ADDQ	AX, R8

  995. 	ADCQ	DX, R9

  996. 	ADCQ	$0, R10

  997. 

  998. 	MOVQ	(16)(REG_P2), AX

  999. 	MULQ	R11

  1000. 	ADDQ	AX, R8

  1001. 	ADCQ	DX, R9

  1002. 	ADCQ	$0, R10

  1003. 

  1004. 	MOVQ	(32)(REG_P2), AX

  1005. 	MULQ	R13

  1006. 	ADDQ	AX, R8

  1007. 	ADCQ	DX, R9

  1008. 	ADCQ	$0, R10

  1009. 

  1010. 	MOVQ	(24)(REG_P2), AX

  1011. 	MULQ	R15

  1012. 	ADDQ	AX, R8

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

  1014. 	ADCQ	DX, R9

  1015. 	ADCQ	$0, R10

  1016. 

  1017. 	XORQ	R8, R8

  1018. 	MOVQ	(24)(REG_P2), AX

  1019. 	MULQ	R11

  1020. 	ADDQ	AX, R9

  1021. 	ADCQ	DX, R10

  1022. 	ADCQ	$0, R8

  1023. 

  1024. 	MOVQ	(32)(REG_P2), AX

  1025. 	MULQ	R15

  1026. 	ADDQ	AX, R9

  1027. 	ADCQ	DX, R10

  1028. 	ADCQ	$0, R8

  1029. 

  1030. 	MOVQ	(40)(REG_P2), AX

  1031. 	MULQ	R13

  1032. 	ADDQ	AX, R9

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

  1034. 	ADCQ	DX, R10

  1035. 	ADCQ	$0, R8

  1036. 

  1037. 	XORQ	R9, R9

  1038. 	MOVQ	(40)(REG_P2), AX

  1039. 	MULQ	R15

  1040. 	ADDQ	AX, R10

  1041. 	ADCQ	DX, R8

  1042. 	ADCQ	$0, R9

  1043. 

  1044. 	MOVQ	(32)(REG_P2), AX

  1045. 	MULQ	R11

  1046. 	ADDQ	AX, R10

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

  1048. 	ADCQ	DX, R8

  1049. 	ADCQ	$0, R9

  1050. 

  1051. 	MOVQ	(40)(REG_P2), AX

  1052. 	MULQ	R11

  1053. 	ADDQ	AX, R8

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

  1055. 	ADCQ	DX, R9

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

  1057. 

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

  1059. 	MOVQ	(48)(REG_P1), R11

  1060. 	MOVQ	(48)(REG_P2), AX

  1061. 	MULQ	R11

  1062. 	XORQ	R9, R9

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

  1064. 	MOVQ	DX, R8

  1065. 

  1066. 	MOVQ	(56)(REG_P2), AX

  1067. 	MULQ	R11

  1068. 	XORQ	R10, R10

  1069. 	ADDQ	AX, R8

  1070. 	ADCQ	DX, R9

  1071. 

  1072. 	MOVQ	(56)(REG_P1), R12

  1073. 	MOVQ	(48)(REG_P2), AX

  1074. 	MULQ	R12

  1075. 	ADDQ	AX, R8

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

  1077. 	ADCQ	DX, R9

  1078. 	ADCQ	$0, R10

  1079. 

  1080. 	XORQ	R8, R8

  1081. 	MOVQ	(64)(REG_P2), AX

  1082. 	MULQ	R11

  1083. 	ADDQ	AX, R9

  1084. 	ADCQ	DX, R10

  1085. 	ADCQ	$0, R8

  1086. 

  1087. 	MOVQ	(48)(REG_P2), R13

  1088. 	MOVQ	(64)(REG_P1), AX

  1089. 	MULQ	R13

  1090. 	ADDQ	AX, R9

  1091. 	ADCQ	DX, R10

  1092. 	ADCQ	$0, R8

  1093. 

  1094. 	MOVQ	(56)(REG_P2), AX

  1095. 	MULQ	R12

  1096. 	ADDQ	AX, R9

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

  1098. 	ADCQ	DX, R10

  1099. 	ADCQ	$0, R8

  1100. 

  1101. 	XORQ	R9, R9

  1102. 	MOVQ	(72)(REG_P2), AX

  1103. 	MULQ	R11

  1104. 	ADDQ	AX, R10

  1105. 	ADCQ	DX, R8

  1106. 	ADCQ	$0, R9

  1107. 

  1108. 	MOVQ	(72)(REG_P1), AX

  1109. 	MULQ	R13

  1110. 	ADDQ	AX, R10

  1111. 	ADCQ	DX, R8

  1112. 	ADCQ	$0, R9

  1113. 

  1114. 	MOVQ	(64)(REG_P2), AX

  1115. 	MULQ	R12

  1116. 	ADDQ	AX, R10

  1117. 	ADCQ	DX, R8

  1118. 	ADCQ	$0, R9

  1119. 

  1120. 	MOVQ	(64)(REG_P1), R14

  1121. 	MOVQ	(56)(REG_P2), AX

  1122. 	MULQ	R14

  1123. 	ADDQ	AX, R10

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

  1125. 	ADCQ	DX, R8

  1126. 	ADCQ	$0, R9

  1127. 

  1128. 	XORQ	R10, R10

  1129. 	MOVQ	(80)(REG_P2), AX

  1130. 	MULQ	R11

  1131. 	ADDQ	AX, R8

  1132. 	ADCQ	DX, R9

  1133. 	ADCQ	$0, R10

  1134. 

  1135. 	MOVQ	(64)(REG_P2), AX

  1136. 	MULQ	R14

  1137. 	ADDQ	AX, R8

  1138. 	ADCQ	DX, R9

  1139. 	ADCQ	$0, R10

  1140. 

  1141. 	MOVQ	(80)(REG_P1), R15

  1142. 	MOVQ	R13, AX

  1143. 	MULQ	R15

  1144. 	ADDQ	AX, R8

  1145. 	ADCQ	DX, R9

  1146. 	ADCQ	$0, R10

  1147. 

  1148. 	MOVQ	(72)(REG_P2), AX

  1149. 	MULQ	R12

  1150. 	ADDQ	AX, R8

  1151. 	ADCQ	DX, R9

  1152. 	ADCQ	$0, R10

  1153. 

  1154. 	MOVQ	(72)(REG_P1), R13

  1155. 	MOVQ	(56)(REG_P2), AX

  1156. 	MULQ	R13

  1157. 	ADDQ	AX, R8

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

  1159. 	ADCQ	DX, R9

  1160. 	ADCQ	$0, R10

  1161. 

  1162. 	XORQ	R8, R8

  1163. 	MOVQ	(88)(REG_P2), AX

  1164. 	MULQ	R11

  1165. 	ADDQ	AX, R9

  1166. 	ADCQ	DX, R10

  1167. 	ADCQ	$0, R8

  1168. 

  1169. 	MOVQ	(64)(REG_P2), AX

  1170. 	MULQ	R13

  1171. 	ADDQ	AX, R9

  1172. 	ADCQ	DX, R10

  1173. 	ADCQ	$0, R8

  1174. 

  1175. 	MOVQ	(72)(REG_P2), AX

  1176. 	MULQ	R14

  1177. 	ADDQ	AX, R9

  1178. 	ADCQ	DX, R10

  1179. 	ADCQ	$0, R8

  1180. 

  1181. 	MOVQ	(88)(REG_P1), R11

  1182. 	MOVQ	(48)(REG_P2), AX

  1183. 	MULQ	R11

  1184. 	ADDQ	AX, R9

  1185. 	ADCQ	DX, R10

  1186. 	ADCQ	$0, R8

  1187. 

  1188. 	MOVQ	(80)(REG_P2), AX

  1189. 	MULQ	R12

  1190. 	ADDQ	AX, R9

  1191. 	ADCQ	DX, R10

  1192. 	ADCQ	$0, R8

  1193. 

  1194. 	MOVQ	(56)(REG_P2), AX

  1195. 	MULQ	R15

  1196. 	ADDQ	AX, R9

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

  1198. 	ADCQ	DX, R10

  1199. 	ADCQ	$0, R8

  1200. 

  1201. 	XORQ	R9, R9

  1202. 	MOVQ	(64)(REG_P2), AX

  1203. 	MULQ	R15

  1204. 	ADDQ	AX, R10

  1205. 	ADCQ	DX, R8

  1206. 	ADCQ	$0, R9

  1207. 

  1208. 	MOVQ	(88)(REG_P2), AX

  1209. 	MULQ	R12

  1210. 	ADDQ	AX, R10

  1211. 	ADCQ	DX, R8

  1212. 	ADCQ	$0, R9

  1213. 

  1214. 	MOVQ	(80)(REG_P2), AX

  1215. 	MULQ	R14

  1216. 	ADDQ	AX, R10

  1217. 	ADCQ	DX, R8

  1218. 	ADCQ	$0, R9

  1219. 

  1220. 	MOVQ	(56)(REG_P2), AX

  1221. 	MULQ	R11

  1222. 	ADDQ	AX, R10

  1223. 	ADCQ	DX, R8

  1224. 	ADCQ	$0, R9

  1225. 

  1226. 	MOVQ	(72)(REG_P2), AX

  1227. 	MULQ	R13

  1228. 	ADDQ	AX, R10

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

  1230. 	ADCQ	DX, R8

  1231. 	ADCQ	$0, R9

  1232. 

  1233. 	XORQ	R10, R10

  1234. 	MOVQ	(88)(REG_P2), AX

  1235. 	MULQ	R14

  1236. 	ADDQ	AX, R8

  1237. 	ADCQ	DX, R9

  1238. 	ADCQ	$0, R10

  1239. 

  1240. 	MOVQ	(64)(REG_P2), AX

  1241. 	MULQ	R11

  1242. 	ADDQ	AX, R8

  1243. 	ADCQ	DX, R9

  1244. 	ADCQ	$0, R10

  1245. 

  1246. 	MOVQ	(80)(REG_P2), AX

  1247. 	MULQ	R13

  1248. 	ADDQ	AX, R8

  1249. 	ADCQ	DX, R9

  1250. 	ADCQ	$0, R10

  1251. 

  1252. 	MOVQ	(72)(REG_P2), AX

  1253. 	MULQ	R15

  1254. 	ADDQ	AX, R8

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

  1256. 	ADCQ	DX, R9

  1257. 	ADCQ	$0, R10

  1258. 

  1259. 	XORQ	R8, R8

  1260. 	MOVQ	(72)(REG_P2), AX

  1261. 	MULQ	R11

  1262. 	ADDQ	AX, R9

  1263. 	ADCQ	DX, R10

  1264. 	ADCQ	$0, R8

  1265. 

  1266. 	MOVQ	(80)(REG_P2), AX

  1267. 	MULQ	R15

  1268. 	ADDQ	AX, R9

  1269. 	ADCQ	DX, R10

  1270. 	ADCQ	$0, R8

  1271. 

  1272. 	MOVQ	(88)(REG_P2), AX

  1273. 	MULQ	R13

  1274. 	ADDQ	AX, R9

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

  1276. 	ADCQ	DX, R10

  1277. 	ADCQ	$0, R8

  1278. 

  1279. 	MOVQ	(88)(REG_P2), AX

  1280. 	MULQ	R15

  1281. 	ADDQ	AX, R10

  1282. 	ADCQ	DX, R8

  1283. 

  1284. 	MOVQ	(80)(REG_P2), AX

  1285. 	MULQ	R11

  1286. 	ADDQ	AX, R10

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

  1288. 	ADCQ	DX, R8

  1289. 

  1290. 	MOVQ	(88)(REG_P2), AX

  1291. 	MULQ	R11

  1292. 	ADDQ	AX, R8

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

  1294. 	ADCQ	$0, DX

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

  1296. 

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

  1298. 	MOVQ	(SP), R8

  1299. 	SUBQ	(CX), R8

  1300. 	MOVQ	(8)(SP), R9

  1301. 	SBBQ	(8)(CX), R9

  1302. 	MOVQ	(16)(SP), R10

  1303. 	SBBQ	(16)(CX), R10

  1304. 	MOVQ	(24)(SP), R11

  1305. 	SBBQ	(24)(CX), R11

  1306. 	MOVQ	(32)(SP), R12

  1307. 	SBBQ	(32)(CX), R12

  1308. 	MOVQ	(40)(SP), R13

  1309. 	SBBQ	(40)(CX), R13

  1310. 	MOVQ	(48)(SP), R14

  1311. 	SBBQ	(48)(CX), R14

  1312. 	MOVQ	(56)(SP), R15

  1313. 	SBBQ	(56)(CX), R15

  1314. 	MOVQ	(64)(SP), AX

  1315. 	SBBQ	(64)(CX), AX

  1316. 	MOVQ	(72)(SP), DX

  1317. 	SBBQ	(72)(CX), DX

  1318. 	MOVQ	(80)(SP), DI

  1319. 	SBBQ	(80)(CX), DI

  1320. 	MOVQ	(88)(SP), SI

  1321. 	SBBQ	(88)(CX), SI

  1322. 	MOVQ	SI, (SP)

  1323. 

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

  1325. 	MOVQ	(96)(CX), SI

  1326. 	SUBQ	SI, R8

  1327. 	MOVQ	(104)(CX), SI

  1328. 	SBBQ	SI, R9

  1329. 	MOVQ	(112)(CX), SI

  1330. 	SBBQ	SI, R10

  1331. 	MOVQ	(120)(CX), SI

  1332. 	SBBQ	SI, R11

  1333. 	MOVQ	(128)(CX), SI

  1334. 	SBBQ	SI, R12

  1335. 	MOVQ	(136)(CX), SI

  1336. 	SBBQ	SI, R13

  1337. 	MOVQ	(144)(CX), SI

  1338. 	SBBQ	SI, R14

  1339. 	MOVQ	(152)(CX), SI

  1340. 	SBBQ	SI, R15

  1341. 	MOVQ	(160)(CX), SI

  1342. 	SBBQ	SI, AX

  1343. 	MOVQ	(168)(CX), SI

  1344. 	SBBQ	SI, DX

  1345. 	MOVQ	(176)(CX), SI

  1346. 	SBBQ	SI, DI

  1347. 	MOVQ	(SP), SI

  1348. 	SBBQ	(184)(CX), SI

  1349. 

  1350. 	// FINAL RESULT

  1351. 	ADDQ	(48)(CX), R8

  1352. 	MOVQ	R8, (48)(CX)

  1353. 	ADCQ	(56)(CX), R9

  1354. 	MOVQ	R9, (56)(CX)

  1355. 	ADCQ	(64)(CX), R10

  1356. 	MOVQ	R10, (64)(CX)

  1357. 	ADCQ	(72)(CX), R11

  1358. 	MOVQ	R11, (72)(CX)

  1359. 	ADCQ	(80)(CX), R12

  1360. 	MOVQ	R12, (80)(CX)

  1361. 	ADCQ	(88)(CX), R13

  1362. 	MOVQ	R13, (88)(CX)

  1363. 	ADCQ	(96)(CX), R14

  1364. 	MOVQ	R14, (96)(CX)

  1365. 	ADCQ	(104)(CX), R15

  1366. 	MOVQ	R15, (104)(CX)

  1367. 	ADCQ	(112)(CX), AX

  1368. 	MOVQ	AX, (112)(CX)

  1369. 	ADCQ	(120)(CX), DX

  1370. 	MOVQ	DX, (120)(CX)

  1371. 	ADCQ	(128)(CX), DI

  1372. 	MOVQ	DI, (128)(CX)

  1373. 	ADCQ	(136)(CX), SI

  1374. 	MOVQ	SI, (136)(CX)

  1375. 	MOVQ	(144)(CX), AX

  1376. 	ADCQ	$0, AX

  1377. 	MOVQ	AX, (144)(CX)

  1378. 	MOVQ	(152)(CX), AX

  1379. 	ADCQ	$0, AX

  1380. 	MOVQ	AX, (152)(CX)

  1381. 	MOVQ	(160)(CX), AX

  1382. 	ADCQ	$0, AX

  1383. 	MOVQ	AX, (160)(CX)

  1384. 	MOVQ	(168)(CX), AX

  1385. 	ADCQ	$0, AX

  1386. 	MOVQ	AX, (168)(CX)

  1387. 	MOVQ	(176)(CX), AX

  1388. 	ADCQ	$0, AX

  1389. 	MOVQ	AX, (176)(CX)

  1390. 	MOVQ	(184)(CX), AX

  1391. 	ADCQ	$0, AX

  1392. 	MOVQ	AX, (184)(CX)

  1393. 

  1394. 	RET

  1395. 

  1396. // This multiplies a 256-bit number pointed to by M0 with p751+1.

  1397. // It is assumed that M1 points to p751+1 stored as a 768-bit Fp751Element.

  1398. // C points to the place to store the result and should be at least 192 bits.

  1399. // This should only be used when the BMI2 and ADX instruction set extensions

  1400. // are available.

  1401. #define mul256x448bmi2adx(M0, M1, C, T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10) \

  1402. 	MOVQ	0+M0, DX		\

  1403. 	MULXQ	M1+40(SB), T1, T0	\

  1404. 	MULXQ	M1+48(SB), T3, T2	\

  1405. 	MOVQ	T1, 0+C			\	// C0_final

  1406. 	XORQ	AX, AX			\

  1407. 	MULXQ	M1+56(SB), T5, T4	\

  1408. 	ADOXQ	T3, T0			\

  1409. 	ADOXQ	T5, T2			\

  1410. 	MULXQ	M1+64(SB), T3, T1	\

  1411. 	ADOXQ	T3, T4			\

  1412. 	MULXQ	M1+72(SB), T6, T5	\

  1413. 	ADOXQ	T6, T1			\

  1414. 	MULXQ	M1+80(SB), T7, T3	\

  1415. 	ADOXQ	T7, T5			\

  1416. 	MULXQ	M1+88(SB), T8, T6	\

  1417. 	ADOXQ	T8, T3			\

  1418. 	ADOXQ	AX, T6			\

  1419. 					\

  1420. 	MOVQ	8+M0, DX		\

  1421. 	MULXQ	M1+40(SB), T7, T8	\

  1422. 	XORQ	AX, AX			\

  1423. 	ADCXQ	T7, T0			\

  1424. 	MOVQ	T0, 8+C			\	// C1_final

  1425. 	ADCXQ	T8, T2			\

  1426. 	MULXQ	M1+48(SB), T8, T7	\

  1427. 	ADOXQ	T8, T2			\

  1428. 	ADCXQ	T7, T4			\

  1429. 	MULXQ	M1+56(SB), T8, T0	\

  1430. 	ADOXQ	T8, T4			\

  1431. 	ADCXQ	T1, T0			\

  1432. 	MULXQ	M1+64(SB), T7, T1	\

  1433. 	ADCXQ	T5, T1			\

  1434. 	MULXQ	M1+72(SB), T8, T5	\

  1435. 	ADCXQ	T5, T3			\

  1436. 	MULXQ	M1+80(SB), T9, T5	\

  1437. 	ADCXQ	T5, T6			\

  1438. 	MULXQ	M1+88(SB), DX, T5	\

  1439. 	ADCXQ	AX, T5			\

  1440. 					\

  1441. 	ADOXQ	T7, T0			\

  1442. 	ADOXQ	T8, T1			\

  1443. 	ADOXQ	T9, T3			\

  1444. 	ADOXQ	DX, T6			\

  1445. 	ADOXQ	AX, T5			\

  1446. 					\

  1447. 	MOVQ	16+M0, DX		\

  1448. 	MULXQ	M1+40(SB), T7, T8	\

  1449. 	XORQ	AX, AX			\

  1450. 	ADCXQ	T7, T2			\

  1451. 	MOVQ	T2, 16+C		\	// C2_final

  1452. 	ADCXQ	T8, T4			\

  1453. 	MULXQ	M1+48(SB), T7, T8	\

  1454. 	ADOXQ	T7, T4			\

  1455. 	ADCXQ	T8, T0			\

  1456. 	MULXQ	M1+56(SB), T8, T2	\

  1457. 	ADOXQ	T8, T0			\

  1458. 	ADCXQ	T2, T1			\

  1459. 	MULXQ	M1+64(SB), T7, T2	\

  1460. 	ADCXQ	T2, T3			\

  1461. 	MULXQ	M1+72(SB), T8, T2	\

  1462. 	ADCXQ	T2, T6			\

  1463. 	MULXQ	M1+80(SB), T9, T2	\

  1464. 	ADCXQ	T2, T5			\

  1465. 	MULXQ	M1+88(SB), DX, T2	\

  1466. 	ADCXQ	AX, T2			\

  1467. 					\

  1468. 	ADOXQ	T7, T1			\

  1469. 	ADOXQ	T8, T3			\

  1470. 	ADOXQ	T9, T6			\

  1471. 	ADOXQ	DX, T5			\

  1472. 	ADOXQ	AX, T2			\

  1473. 					\

  1474. 	MOVQ	24+M0, DX		\

  1475. 	MULXQ	M1+40(SB), T7, T8	\

  1476. 	XORQ	AX, AX			\

  1477. 	ADCXQ	T4, T7			\

  1478. 	ADCXQ	T8, T0			\

  1479. 	MULXQ	M1+48(SB), T10, T8	\

  1480. 	ADOXQ	T10, T0			\

  1481. 	ADCXQ	T8, T1			\

  1482. 	MULXQ	M1+56(SB), T8, T4	\

  1483. 	ADOXQ	T8, T1			\

  1484. 	ADCXQ	T4, T3			\

  1485. 	MULXQ	M1+64(SB), T10, T4	\

  1486. 	ADCXQ	T4, T6			\

  1487. 	MULXQ	M1+72(SB), T8, T4	\

  1488. 	ADCXQ	T4, T5			\

  1489. 	MULXQ	M1+80(SB), T9, T4	\

  1490. 	ADCXQ	T4, T2			\

  1491. 	MULXQ	M1+88(SB), DX, T4	\

  1492. 	ADCXQ	AX, T4			\

  1493. 					\

  1494. 	ADOXQ	T10, T3			\

  1495. 	ADOXQ	T8, T6			\

  1496. 	ADOXQ	T9, T5			\

  1497. 	ADOXQ	DX, T2			\

  1498. 	ADOXQ	AX, T4

  1499. 

  1500. // This multiplies a 256-bit number pointed to by M0 with p751+1.

  1501. // It is assumed that M1 points to p751+1 stored as a 768-bit Fp751Element.

  1502. // C points to the place to store the result and should be at least 192 bits.

  1503. // This should only be used when the BMI2 instruction set extension is

  1504. // available.

  1505. #define mul256x448bmi2(M0, M1, C, T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10) \

  1506. 	MOVQ	0+M0, DX		\

  1507. 	MULXQ	M1+40(SB), T1, T0	\

  1508. 	MULXQ	M1+48(SB), T3, T2	\

  1509. 	MOVQ	T1, 0+C			\	// C0_final

  1510. 	XORQ	AX, AX			\

  1511. 	MULXQ	M1+56(SB), T5, T4	\

  1512. 	ADDQ	T3, T0			\

  1513. 	ADCQ	T5, T2			\

  1514. 	MULXQ	M1+64(SB), T3, T1	\

  1515. 	ADCQ	T3, T4			\

  1516. 	MULXQ	M1+72(SB), T6, T5	\

  1517. 	ADCQ	T6, T1			\

  1518. 	MULXQ	M1+80(SB), T7, T3	\

  1519. 	ADCQ	T7, T5			\

  1520. 	MULXQ	M1+88(SB), T8, T6	\

  1521. 	ADCQ	T8, T3			\

  1522. 	ADCQ	AX, T6			\

  1523. 					\

  1524. 	MOVQ	8+M0, DX		\

  1525. 	MULXQ	M1+40(SB), T7, T8	\

  1526. 	ADDQ	T7, T0			\

  1527. 	MOVQ	T0, 8+C			\	// C1_final

  1528. 	ADCQ	T8, T2			\

  1529. 	MULXQ	M1+48(SB), T8, T7	\

  1530. 	MOVQ	T8, 32+C		\

  1531. 	ADCQ	T7, T4			\

  1532. 	MULXQ	M1+56(SB), T8, T0	\

  1533. 	MOVQ	T8, 40+C		\

  1534. 	ADCQ	T1, T0			\

  1535. 	MULXQ	M1+64(SB), T7, T1	\

  1536. 	ADCQ	T5, T1			\

  1537. 	MULXQ	M1+72(SB), T8, T5	\

  1538. 	ADCQ	T5, T3			\

  1539. 	MULXQ	M1+80(SB), T9, T5	\

  1540. 	ADCQ	T5, T6			\

  1541. 	MULXQ	M1+88(SB), DX, T5	\

  1542. 	ADCQ	AX, T5			\

  1543. 					\

  1544. 	XORQ	AX, AX			\

  1545. 	ADDQ	32+C, T2		\

  1546. 	ADCQ	40+C, T4		\

  1547. 	ADCQ	T7, T0			\

  1548. 	ADCQ	T8, T1			\

  1549. 	ADCQ	T9, T3			\

  1550. 	ADCQ	DX, T6			\

  1551. 	ADCQ	AX, T5			\

  1552. 					\

  1553. 	MOVQ	16+M0, DX		\

  1554. 	MULXQ	M1+40(SB), T7, T8	\

  1555. 	ADDQ	T7, T2			\

  1556. 	MOVQ	T2, 16+C		\	// C2_final

  1557. 	ADCQ	T8, T4			\

  1558. 	MULXQ	M1+48(SB), T7, T8	\

  1559. 	MOVQ	T7, 32+C		\

  1560. 	ADCQ	T8, T0			\

  1561. 	MULXQ	M1+56(SB), T8, T2	\

  1562. 	MOVQ	T8, 40+C		\

  1563. 	ADCQ	T2, T1			\

  1564. 	MULXQ	M1+64(SB), T7, T2	\

  1565. 	ADCQ	T2, T3			\

  1566. 	MULXQ	M1+72(SB), T8, T2	\

  1567. 	ADCQ	T2, T6			\

  1568. 	MULXQ	M1+80(SB), T9, T2	\

  1569. 	ADCQ	T2, T5			\

  1570. 	MULXQ	M1+88(SB), DX, T2	\

  1571. 	ADCQ	AX, T2			\

  1572. 					\

  1573. 	XORQ	AX, AX			\

  1574. 	ADDQ	32+C, T4		\

  1575. 	ADCQ	40+C, T0		\

  1576. 	ADCQ	T7, T1			\

  1577. 	ADCQ	T8, T3			\

  1578. 	ADCQ	T9, T6			\

  1579. 	ADCQ	DX, T5			\

  1580. 	ADCQ	AX, T2			\

  1581. 					\

  1582. 	MOVQ	24+M0, DX		\

  1583. 	MULXQ	M1+40(SB), T7, T8	\

  1584. 	ADDQ	T4, T7			\

  1585. 	ADCQ	T8, T0			\

  1586. 	MULXQ	M1+48(SB), T10, T8	\

  1587. 	MOVQ	T10, 32+C		\

  1588. 	ADCQ	T8, T1			\

  1589. 	MULXQ	M1+56(SB), T8, T4	\

  1590. 	MOVQ	T8, 40+C		\

  1591. 	ADCQ	T4, T3			\

  1592. 	MULXQ	M1+64(SB), T10, T4	\

  1593. 	ADCQ	T4, T6			\

  1594. 	MULXQ	M1+72(SB), T8, T4	\

  1595. 	ADCQ	T4, T5			\

  1596. 	MULXQ	M1+80(SB), T9, T4	\

  1597. 	ADCQ	T4, T2			\

  1598. 	MULXQ	M1+88(SB), DX, T4	\

  1599. 	ADCQ	AX, T4			\

  1600. 					\

  1601. 	XORQ	AX, AX			\

  1602. 	ADDQ	32+C, T0		\

  1603. 	ADCQ	40+C, T1		\

  1604. 	ADCQ	T10, T3			\

  1605. 	ADCQ	T8, T6			\

  1606. 	ADCQ	T9, T5			\

  1607. 	ADCQ	DX, T2			\

  1608. 	ADCQ	AX, T4

  1609. 

  1610. // Template for calculating the Montgomery reduction algorithm described in

  1611. // section 5.2.3 of https://eprint.iacr.org/2017/1015.pdf. Template must be

  1612. // customized with schoolbook multiplicaton for 256 x 448-bit number.

  1613. // This macro reuses memory of IN value and *changes* it. Smashes registers

  1614. // R[8-15], AX, BX, CX, DX, BP.

  1615. // Input:

  1616. //    * M0: 1536-bit number to be reduced

  1617. //    * C : either mul256x448bmi2 or mul256x448bmi2adx

  1618. // Output: OUT 768-bit

  1619. #define REDC(C, M0, MULS) 	\

  1620.     \ // a[0-3] x p751p1_nz --> result: [reg_p2+48], [reg_p2+56], [reg_p2+64], and rbp, r8:r14

  1621.     MULS(M0, ·p751p1, 48+C, R8, R9, R13, R10, R14, R12, R11, BP, BX, CX, R15) \

  1622.     XORQ    R15, R15        \

  1623.     MOVQ    48+C, AX        \

  1624.     MOVQ    56+C, DX        \

  1625.     MOVQ    64+C, BX        \

  1626.     ADDQ    40+M0, AX       \

  1627.     ADCQ    48+M0, DX       \

  1628.     ADCQ    56+M0, BX       \

  1629.     MOVQ    AX, 40+M0       \

  1630.     MOVQ    DX, 48+M0       \

  1631.     MOVQ    BX, 56+M0       \

  1632.     ADCQ    64+M0, BP       \

  1633.     ADCQ    72+M0, R8       \

  1634.     ADCQ    80+M0, R9       \

  1635.     ADCQ    88+M0, R10      \

  1636.     ADCQ    96+M0, R11      \

  1637.     ADCQ    104+M0, R12     \

  1638.     ADCQ    112+M0, R13     \

  1639.     ADCQ    120+M0, R14     \

  1640.     ADCQ    128+M0, R15     \

  1641.     MOVQ    BP, 64+M0       \

  1642.     MOVQ    R8, 72+M0       \

  1643.     MOVQ    R9, 80+M0       \

  1644.     MOVQ    R10, 88+M0      \

  1645.     MOVQ    R11, 96+M0      \

  1646.     MOVQ    R12, 104+M0     \

  1647.     MOVQ    R13, 112+M0     \

  1648.     MOVQ    R14, 120+M0     \

  1649.     MOVQ    R15, 128+M0     \

  1650.     MOVQ    136+M0, R8      \

  1651.     MOVQ    144+M0, R9      \

  1652.     MOVQ    152+M0, R10     \

  1653.     MOVQ    160+M0, R11     \

  1654.     MOVQ    168+M0, R12     \

  1655.     MOVQ    176+M0, R13     \

  1656.     MOVQ    184+M0, R14     \

  1657.     ADCQ    $0, R8          \

  1658.     ADCQ    $0, R9          \

  1659.     ADCQ    $0, R10         \

  1660.     ADCQ    $0, R11         \

  1661.     ADCQ    $0, R12         \

  1662.     ADCQ    $0, R13         \

  1663.     ADCQ    $0, R14         \

  1664.     MOVQ    R8, 136+M0      \

  1665.     MOVQ    R9, 144+M0      \

  1666.     MOVQ    R10, 152+M0     \

  1667.     MOVQ    R11, 160+M0     \

  1668.     MOVQ    R12, 168+M0     \

  1669.     MOVQ    R13, 176+M0     \

  1670.     MOVQ    R14, 184+M0     \

  1671.     \ // a[4-7] x p751p1_nz --> result: [reg_p2+48], [reg_p2+56], [reg_p2+64], and rbp, r8:r14

  1672.     MULS(32+M0, ·p751p1, 48+C, R8, R9, R13, R10, R14, R12, R11, BP, BX, CX, R15) \

  1673.     XORQ    R15, R15          \

  1674.     MOVQ    48+C, AX        \

  1675.     MOVQ    56+C, DX        \

  1676.     MOVQ    64+C, BX        \

  1677.     ADDQ    72+M0, AX       \

  1678.     ADCQ    80+M0, DX       \

  1679.     ADCQ    88+M0, BX       \

  1680.     MOVQ    AX, 72+M0       \

  1681.     MOVQ    DX, 80+M0       \

  1682.     MOVQ    BX, 88+M0       \

  1683.     ADCQ    96+M0, BP       \

  1684.     ADCQ    104+M0, R8      \

  1685.     ADCQ    112+M0, R9      \

  1686.     ADCQ    120+M0, R10     \

  1687.     ADCQ    128+M0, R11     \

  1688.     ADCQ    136+M0, R12     \

  1689.     ADCQ    144+M0, R13     \

  1690.     ADCQ    152+M0, R14     \

  1691.     ADCQ    160+M0, R15     \

  1692.     MOVQ    BP, 0+C         \   // Final result c0

  1693.     MOVQ    R8, 104+M0      \

  1694.     MOVQ    R9, 112+M0      \

  1695.     MOVQ    R10, 120+M0     \

  1696.     MOVQ    R11, 128+M0     \

  1697.     MOVQ    R12, 136+M0     \

  1698.     MOVQ    R13, 144+M0     \

  1699.     MOVQ    R14, 152+M0     \

  1700.     MOVQ    R15, 160+M0     \

  1701.     MOVQ    168+M0, R12     \

  1702.     MOVQ    176+M0, R13     \

  1703.     MOVQ    184+M0, R14     \

  1704.     ADCQ    $0, R12         \

  1705.     ADCQ    $0, R13         \

  1706.     ADCQ    $0, R14         \

  1707.     MOVQ    R12, 168+M0     \

  1708.     MOVQ    R13, 176+M0     \

  1709.     MOVQ    R14, 184+M0     \

  1710.     \ // a[8-11] x p751p1_nz --> result: [reg_p2+48], [reg_p2+56], [reg_p2+64], and rbp, r8:r14

  1711.     MULS(64+M0, ·p751p1, 48+C, R8, R9, R13, R10, R14, R12, R11, BP, BX, CX, R15) \

  1712.     MOVQ    48+C, AX        \   // Final result c1:c11

  1713.     MOVQ    56+C, DX        \

  1714.     MOVQ    64+C, BX        \

  1715.     ADDQ    104+M0, AX      \

  1716.     ADCQ    112+M0, DX      \

  1717.     ADCQ    120+M0, BX      \

  1718.     MOVQ    AX, 8+C         \

  1719.     MOVQ    DX, 16+C        \

  1720.     MOVQ    BX, 24+C        \

  1721.     ADCQ    128+M0, BP      \

  1722.     ADCQ    136+M0, R8      \

  1723.     ADCQ    144+M0, R9      \

  1724.     ADCQ    152+M0, R10     \

  1725.     ADCQ    160+M0, R11     \

  1726.     ADCQ    168+M0, R12     \

  1727.     ADCQ    176+M0, R13     \

  1728.     ADCQ    184+M0, R14     \

  1729.     MOVQ    BP, 32+C        \

  1730.     MOVQ    R8, 40+C        \

  1731.     MOVQ    R9, 48+C        \

  1732.     MOVQ    R10, 56+C       \

  1733.     MOVQ    R11, 64+C       \

  1734.     MOVQ    R12, 72+C       \

  1735.     MOVQ    R13, 80+C       \

  1736.     MOVQ    R14, 88+C

  1737. 

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

  1739. 	MOVQ z+0(FP), REG_P2

  1740. 	MOVQ x+8(FP), REG_P1

  1741. 

  1742. 	// Check wether to use optimized implementation

  1743. 	CMPB    github·com∕cloudflare∕sidh∕internal∕utils·HasADXandBMI2(SB), $1

  1744. 	JE      redc_with_mulx_adcx_adox

  1745. 	CMPB    github·com∕cloudflare∕sidh∕internal∕utils·HasBMI2(SB), $1

  1746. 	JE      redc_with_mulx

  1747. 

  1748. 	MOVQ	(REG_P1), R11

  1749. 	MOVQ	P751P1_5, AX

  1750. 	MULQ	R11

  1751. 	XORQ	R8, R8

  1752. 	ADDQ	(40)(REG_P1), AX

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

  1754. 	ADCQ	DX, R8

  1755. 

  1756. 	XORQ	R9, R9

  1757. 	MOVQ	P751P1_6, AX

  1758. 	MULQ	R11

  1759. 	XORQ	R10, R10

  1760. 	ADDQ	AX, R8

  1761. 	ADCQ	DX, R9

  1762. 

  1763. 	MOVQ	(8)(REG_P1), R12

  1764. 	MOVQ	P751P1_5, AX

  1765. 	MULQ	R12

  1766. 	ADDQ	AX, R8

  1767. 	ADCQ	DX, R9

  1768. 	ADCQ	$0, R10

  1769. 	ADDQ	(48)(REG_P1), R8

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

  1771. 	ADCQ	$0, R9

  1772. 	ADCQ	$0, R10

  1773. 

  1774. 	XORQ	R8, R8

  1775. 	MOVQ	P751P1_7, AX

  1776. 	MULQ	R11

  1777. 	ADDQ	AX, R9

  1778. 	ADCQ	DX, R10

  1779. 	ADCQ	$0, R8

  1780. 

  1781. 	MOVQ	P751P1_6, AX

  1782. 	MULQ	R12

  1783. 	ADDQ	AX, R9

  1784. 	ADCQ	DX, R10

  1785. 	ADCQ	$0, R8

  1786. 

  1787. 	MOVQ	(16)(REG_P1), R13

  1788. 	MOVQ	P751P1_5, AX

  1789. 	MULQ	R13

  1790. 	ADDQ	AX, R9

  1791. 	ADCQ	DX, R10

  1792. 	ADCQ	$0, R8

  1793. 	ADDQ	(56)(REG_P1), R9

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

  1795. 	ADCQ	$0, R10

  1796. 	ADCQ	$0, R8

  1797. 

  1798. 	XORQ	R9, R9

  1799. 	MOVQ	P751P1_8, AX

  1800. 	MULQ	R11

  1801. 	ADDQ	AX, R10

  1802. 	ADCQ	DX, R8

  1803. 	ADCQ	$0, R9

  1804. 

  1805. 	MOVQ	P751P1_7, AX

  1806. 	MULQ	R12

  1807. 	ADDQ	AX, R10

  1808. 	ADCQ	DX, R8

  1809. 	ADCQ	$0, R9

  1810. 

  1811. 	MOVQ	P751P1_6, AX

  1812. 	MULQ	R13

  1813. 	ADDQ	AX, R10

  1814. 	ADCQ	DX, R8

  1815. 	ADCQ	$0, R9

  1816. 

  1817. 	MOVQ	(24)(REG_P1), R14

  1818. 	MOVQ	P751P1_5, AX

  1819. 	MULQ	R14

  1820. 	ADDQ	AX, R10

  1821. 	ADCQ	DX, R8

  1822. 	ADCQ	$0, R9

  1823. 	ADDQ	(64)(REG_P1), R10

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

  1825. 	ADCQ	$0, R8

  1826. 	ADCQ	$0, R9

  1827. 

  1828. 	XORQ	R10, R10

  1829. 	MOVQ	P751P1_9, AX

  1830. 	MULQ	R11

  1831. 	ADDQ	AX, R8

  1832. 	ADCQ	DX, R9

  1833. 	ADCQ	$0, R10

  1834. 

  1835. 	MOVQ	P751P1_8, AX

  1836. 	MULQ	R12

  1837. 	ADDQ	AX, R8

  1838. 	ADCQ	DX, R9

  1839. 	ADCQ	$0, R10

  1840. 

  1841. 	MOVQ	P751P1_7, AX

  1842. 	MULQ	R13

  1843. 	ADDQ	AX, R8

  1844. 	ADCQ	DX, R9

  1845. 	ADCQ	$0, R10

  1846. 

  1847. 	MOVQ	P751P1_6, AX

  1848. 	MULQ	R14

  1849. 	ADDQ	AX, R8

  1850. 	ADCQ	DX, R9

  1851. 	ADCQ	$0, R10

  1852. 

  1853. 	MOVQ	(32)(REG_P1), R15

  1854. 	MOVQ	P751P1_5, AX

  1855. 	MULQ	R15

  1856. 	ADDQ	AX, R8

  1857. 	ADCQ	DX, R9

  1858. 	ADCQ	$0, R10

  1859. 	ADDQ	(72)(REG_P1), R8

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

  1861. 	ADCQ	$0, R9

  1862. 	ADCQ	$0, R10

  1863. 

  1864. 	XORQ	R8, R8

  1865. 	MOVQ	P751P1_10, AX

  1866. 	MULQ	R11

  1867. 	ADDQ	AX, R9

  1868. 	ADCQ	DX, R10

  1869. 	ADCQ	$0, R8

  1870. 

  1871. 	MOVQ	P751P1_9, AX

  1872. 	MULQ	R12

  1873. 	ADDQ	AX, R9

  1874. 	ADCQ	DX, R10

  1875. 	ADCQ	$0, R8

  1876. 

  1877. 	MOVQ	P751P1_8, AX

  1878. 	MULQ	R13

  1879. 	ADDQ	AX, R9

  1880. 	ADCQ	DX, R10

  1881. 	ADCQ	$0, R8

  1882. 

  1883. 	MOVQ	P751P1_7, AX

  1884. 	MULQ	R14

  1885. 	ADDQ	AX, R9

  1886. 	ADCQ	DX, R10

  1887. 	ADCQ	$0, R8

  1888. 

  1889. 	MOVQ	P751P1_6, AX

  1890. 	MULQ	R15

  1891. 	ADDQ	AX, R9

  1892. 	ADCQ	DX, R10

  1893. 	ADCQ	$0, R8

  1894. 

  1895. 	MOVQ	(40)(REG_P2), CX

  1896. 	MOVQ	P751P1_5, AX

  1897. 	MULQ	CX

  1898. 	ADDQ	AX, R9

  1899. 	ADCQ	DX, R10

  1900. 	ADCQ	$0, R8

  1901. 	ADDQ	(80)(REG_P1), R9

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

  1903. 	ADCQ	$0, R10

  1904. 	ADCQ	$0, R8

  1905. 

  1906. 	XORQ	R9, R9

  1907. 	MOVQ	P751P1_11, AX

  1908. 	MULQ	R11

  1909. 	ADDQ	AX, R10

  1910. 	ADCQ	DX, R8

  1911. 	ADCQ	$0, R9

  1912. 

  1913. 	MOVQ	P751P1_10, AX

  1914. 	MULQ	R12

  1915. 	ADDQ	AX, R10

  1916. 	ADCQ	DX, R8

  1917. 	ADCQ	$0, R9

  1918. 

  1919. 	MOVQ	P751P1_9, AX

  1920. 	MULQ	R13

  1921. 	ADDQ	AX, R10

  1922. 	ADCQ	DX, R8

  1923. 	ADCQ	$0, R9

  1924. 

  1925. 	MOVQ	P751P1_8, AX

  1926. 	MULQ	R14

  1927. 	ADDQ	AX, R10

  1928. 	ADCQ	DX, R8

  1929. 	ADCQ	$0, R9

  1930. 

  1931. 	MOVQ	P751P1_7, AX

  1932. 	MULQ	R15

  1933. 	ADDQ	AX, R10

  1934. 	ADCQ	DX, R8

  1935. 	ADCQ	$0, R9

  1936. 

  1937. 	MOVQ	P751P1_6, AX

  1938. 	MULQ	CX

  1939. 	ADDQ	AX, R10

  1940. 	ADCQ	DX, R8

  1941. 	ADCQ	$0, R9

  1942. 

  1943. 	MOVQ	(48)(REG_P2), R11

  1944. 	MOVQ	P751P1_5, AX

  1945. 	MULQ	R11

  1946. 	ADDQ	AX, R10

  1947. 	ADCQ	DX, R8

  1948. 	ADCQ	$0, R9

  1949. 	ADDQ	(88)(REG_P1), R10

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

  1951. 	ADCQ	$0, R8

  1952. 	ADCQ	$0, R9

  1953. 

  1954. 	XORQ	R10, R10

  1955. 	MOVQ	P751P1_11, AX

  1956. 	MULQ	R12

  1957. 	ADDQ	AX, R8

  1958. 	ADCQ	DX, R9

  1959. 	ADCQ	$0, R10

  1960. 

  1961. 	MOVQ	P751P1_10, AX

  1962. 	MULQ	R13

  1963. 	ADDQ	AX, R8

  1964. 	ADCQ	DX, R9

  1965. 	ADCQ	$0, R10

  1966. 

  1967. 	MOVQ	P751P1_9, AX

  1968. 	MULQ	R14

  1969. 	ADDQ	AX, R8

  1970. 	ADCQ	DX, R9

  1971. 	ADCQ	$0, R10

  1972. 

  1973. 	MOVQ	P751P1_8, AX

  1974. 	MULQ	R15

  1975. 	ADDQ	AX, R8

  1976. 	ADCQ	DX, R9

  1977. 	ADCQ	$0, R10

  1978. 

  1979. 	MOVQ	P751P1_7, AX

  1980. 	MULQ	CX

  1981. 	ADDQ	AX, R8

  1982. 	ADCQ	DX, R9

  1983. 	ADCQ	$0, R10

  1984. 

  1985. 	MOVQ	P751P1_6, AX

  1986. 	MULQ	R11

  1987. 	ADDQ	AX, R8

  1988. 	ADCQ	DX, R9

  1989. 	ADCQ	$0, R10

  1990. 

  1991. 	MOVQ	(56)(REG_P2), R12

  1992. 	MOVQ	P751P1_5, AX

  1993. 	MULQ	R12

  1994. 	ADDQ	AX, R8

  1995. 	ADCQ	DX, R9

  1996. 	ADCQ	$0, R10

  1997. 	ADDQ	(96)(REG_P1), R8

  1998. 	MOVQ	R8, (REG_P2)		// Z0

  1999. 	ADCQ	$0, R9

  2000. 	ADCQ	$0, R10

  2001. 

  2002. 	XORQ	R8, R8

  2003. 	MOVQ	P751P1_11, AX

  2004. 	MULQ	R13

  2005. 	ADDQ	AX, R9

  2006. 	ADCQ	DX, R10

  2007. 	ADCQ	$0, R8

  2008. 

  2009. 	MOVQ	P751P1_10, AX

  2010. 	MULQ	R14

  2011. 	ADDQ	AX, R9

  2012. 	ADCQ	DX, R10

  2013. 	ADCQ	$0, R8

  2014. 

  2015. 	MOVQ	P751P1_9, AX

  2016. 	MULQ	R15

  2017. 	ADDQ	AX, R9

  2018. 	ADCQ	DX, R10

  2019. 	ADCQ	$0, R8

  2020. 

  2021. 	MOVQ	P751P1_8, AX

  2022. 	MULQ	CX

  2023. 	ADDQ	AX, R9

  2024. 	ADCQ	DX, R10

  2025. 	ADCQ	$0, R8

  2026. 

  2027. 	MOVQ	P751P1_7, AX

  2028. 	MULQ	R11

  2029. 	ADDQ	AX, R9

  2030. 	ADCQ	DX, R10

  2031. 	ADCQ	$0, R8

  2032. 

  2033. 	MOVQ	P751P1_6, AX

  2034. 	MULQ	R12

  2035. 	ADDQ	AX, R9

  2036. 	ADCQ	DX, R10

  2037. 	ADCQ	$0, R8

  2038. 

  2039. 	MOVQ	(64)(REG_P2), R13

  2040. 	MOVQ	P751P1_5, AX

  2041. 	MULQ	R13

  2042. 	ADDQ	AX, R9

  2043. 	ADCQ	DX, R10

  2044. 	ADCQ	$0, R8

  2045. 	ADDQ	(104)(REG_P1), R9

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

  2047. 	ADCQ	$0, R10

  2048. 	ADCQ	$0, R8

  2049. 

  2050. 	XORQ	R9, R9

  2051. 	MOVQ	P751P1_11, AX

  2052. 	MULQ	R14

  2053. 	ADDQ	AX, R10

  2054. 	ADCQ	DX, R8

  2055. 	ADCQ	$0, R9

  2056. 

  2057. 	MOVQ	P751P1_10, AX

  2058. 	MULQ	R15

  2059. 	ADDQ	AX, R10

  2060. 	ADCQ	DX, R8

  2061. 	ADCQ	$0, R9

  2062. 

  2063. 	MOVQ	P751P1_9, AX

  2064. 	MULQ	CX

  2065. 	ADDQ	AX, R10

  2066. 	ADCQ	DX, R8

  2067. 	ADCQ	$0, R9

  2068. 

  2069. 	MOVQ	P751P1_8, AX

  2070. 	MULQ	R11

  2071. 	ADDQ	AX, R10

  2072. 	ADCQ	DX, R8

  2073. 	ADCQ	$0, R9

  2074. 

  2075. 	MOVQ	P751P1_7, AX

  2076. 	MULQ	R12

  2077. 	ADDQ	AX, R10

  2078. 	ADCQ	DX, R8

  2079. 	ADCQ	$0, R9

  2080. 

  2081. 	MOVQ	P751P1_6, AX

  2082. 	MULQ	R13

  2083. 	ADDQ	AX, R10

  2084. 	ADCQ	DX, R8

  2085. 	ADCQ	$0, R9

  2086. 

  2087. 	MOVQ	(72)(REG_P2), R14

  2088. 	MOVQ	P751P1_5, AX

  2089. 	MULQ	R14

  2090. 	ADDQ	AX, R10

  2091. 	ADCQ	DX, R8

  2092. 	ADCQ	$0, R9

  2093. 	ADDQ	(112)(REG_P1), R10

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

  2095. 	ADCQ	$0, R8

  2096. 	ADCQ	$0, R9

  2097. 

  2098. 	XORQ	R10, R10

  2099. 	MOVQ	P751P1_11, AX

  2100. 	MULQ	R15

  2101. 	ADDQ	AX, R8

  2102. 	ADCQ	DX, R9

  2103. 	ADCQ	$0, R10

  2104. 

  2105. 	MOVQ	P751P1_10, AX

  2106. 	MULQ	CX

  2107. 	ADDQ	AX, R8

  2108. 	ADCQ	DX, R9

  2109. 	ADCQ	$0, R10

  2110. 

  2111. 	MOVQ	P751P1_9, AX

  2112. 	MULQ	R11

  2113. 	ADDQ	AX, R8

  2114. 	ADCQ	DX, R9

  2115. 	ADCQ	$0, R10

  2116. 

  2117. 	MOVQ	P751P1_8, AX

  2118. 	MULQ	R12

  2119. 	ADDQ	AX, R8

  2120. 	ADCQ	DX, R9

  2121. 	ADCQ	$0, R10

  2122. 

  2123. 	MOVQ	P751P1_7, AX

  2124. 	MULQ	R13

  2125. 	ADDQ	AX, R8

  2126. 	ADCQ	DX, R9

  2127. 	ADCQ	$0, R10

  2128. 

  2129. 	MOVQ	P751P1_6, AX

  2130. 	MULQ	R14

  2131. 	ADDQ	AX, R8

  2132. 	ADCQ	DX, R9

  2133. 	ADCQ	$0, R10

  2134. 

  2135. 	MOVQ	(80)(REG_P2), R15

  2136. 	MOVQ	P751P1_5, AX

  2137. 	MULQ	R15

  2138. 	ADDQ	AX, R8

  2139. 	ADCQ	DX, R9

  2140. 	ADCQ	$0, R10

  2141. 	ADDQ	(120)(REG_P1), R8

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

  2143. 	ADCQ	$0, R9

  2144. 	ADCQ	$0, R10

  2145. 

  2146. 	XORQ	R8, R8

  2147. 	MOVQ	P751P1_11, AX

  2148. 	MULQ	CX

  2149. 	ADDQ	AX, R9

  2150. 	ADCQ	DX, R10

  2151. 	ADCQ	$0, R8

  2152. 

  2153. 	MOVQ	P751P1_10, AX

  2154. 	MULQ	R11

  2155. 	ADDQ	AX, R9

  2156. 	ADCQ	DX, R10

  2157. 	ADCQ	$0, R8

  2158. 

  2159. 	MOVQ	P751P1_9, AX

  2160. 	MULQ	R12

  2161. 	ADDQ	AX, R9

  2162. 	ADCQ	DX, R10

  2163. 	ADCQ	$0, R8

  2164. 

  2165. 	MOVQ	P751P1_8, AX

  2166. 	MULQ	R13

  2167. 	ADDQ	AX, R9

  2168. 	ADCQ	DX, R10

  2169. 	ADCQ	$0, R8

  2170. 

  2171. 	MOVQ	P751P1_7, AX

  2172. 	MULQ	R14

  2173. 	ADDQ	AX, R9

  2174. 	ADCQ	DX, R10

  2175. 	ADCQ	$0, R8

  2176. 

  2177. 	MOVQ	P751P1_6, AX

  2178. 	MULQ	R15

  2179. 	ADDQ	AX, R9

  2180. 	ADCQ	DX, R10

  2181. 	ADCQ	$0, R8

  2182. 

  2183. 	MOVQ	(88)(REG_P2), CX

  2184. 	MOVQ	P751P1_5, AX

  2185. 	MULQ	CX

  2186. 	ADDQ	AX, R9

  2187. 	ADCQ	DX, R10

  2188. 	ADCQ	$0, R8

  2189. 	ADDQ	(128)(REG_P1), R9

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

  2191. 	ADCQ	$0, R10

  2192. 	ADCQ	$0, R8

  2193. 

  2194. 	XORQ	R9, R9

  2195. 	MOVQ	P751P1_11, AX

  2196. 	MULQ	R11

  2197. 	ADDQ	AX, R10

  2198. 	ADCQ	DX, R8

  2199. 	ADCQ	$0, R9

  2200. 

  2201. 	MOVQ	P751P1_10, AX

  2202. 	MULQ	R12

  2203. 	ADDQ	AX, R10

  2204. 	ADCQ	DX, R8

  2205. 	ADCQ	$0, R9

  2206. 

  2207. 	MOVQ	P751P1_9, AX

  2208. 	MULQ	R13

  2209. 	ADDQ	AX, R10

  2210. 	ADCQ	DX, R8

  2211. 	ADCQ	$0, R9

  2212. 

  2213. 	MOVQ	P751P1_8, AX

  2214. 	MULQ	R14

  2215. 	ADDQ	AX, R10

  2216. 	ADCQ	DX, R8

  2217. 	ADCQ	$0, R9

  2218. 

  2219. 	MOVQ	P751P1_7, AX

  2220. 	MULQ	R15

  2221. 	ADDQ	AX, R10

  2222. 	ADCQ	DX, R8

  2223. 	ADCQ	$0, R9

  2224. 

  2225. 	MOVQ	P751P1_6, AX

  2226. 	MULQ	CX

  2227. 	ADDQ	AX, R10

  2228. 	ADCQ	DX, R8

  2229. 	ADCQ	$0, R9

  2230. 	ADDQ	(136)(REG_P1), R10

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

  2232. 	ADCQ	$0, R8

  2233. 	ADCQ	$0, R9

  2234. 

  2235. 	XORQ	R10, R10

  2236. 	MOVQ	P751P1_11, AX

  2237. 	MULQ	R12

  2238. 	ADDQ	AX, R8

  2239. 	ADCQ	DX, R9

  2240. 	ADCQ	$0, R10

  2241. 

  2242. 	MOVQ	P751P1_10, AX

  2243. 	MULQ	R13

  2244. 	ADDQ	AX, R8

  2245. 	ADCQ	DX, R9

  2246. 	ADCQ	$0, R10

  2247. 

  2248. 	MOVQ	P751P1_9, AX

  2249. 	MULQ	R14

  2250. 	ADDQ	AX, R8

  2251. 	ADCQ	DX, R9

  2252. 	ADCQ	$0, R10

  2253. 

  2254. 	MOVQ	P751P1_8, AX

  2255. 	MULQ	R15

  2256. 	ADDQ	AX, R8

  2257. 	ADCQ	DX, R9

  2258. 	ADCQ	$0, R10

  2259. 

  2260. 	MOVQ	P751P1_7, AX

  2261. 	MULQ	CX

  2262. 	ADDQ	AX, R8

  2263. 	ADCQ	DX, R9

  2264. 	ADCQ	$0, R10

  2265. 	ADDQ	(144)(REG_P1), R8

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

  2267. 	ADCQ	$0, R9

  2268. 	ADCQ	$0, R10

  2269. 

  2270. 	XORQ	R8, R8

  2271. 	MOVQ	P751P1_11, AX

  2272. 	MULQ	R13

  2273. 	ADDQ	AX, R9

  2274. 	ADCQ	DX, R10

  2275. 	ADCQ	$0, R8

  2276. 

  2277. 	MOVQ	P751P1_10, AX

  2278. 	MULQ	R14

  2279. 	ADDQ	AX, R9

  2280. 	ADCQ	DX, R10

  2281. 	ADCQ	$0, R8

  2282. 

  2283. 	MOVQ	P751P1_9, AX

  2284. 	MULQ	R15

  2285. 	ADDQ	AX, R9

  2286. 	ADCQ	DX, R10

  2287. 	ADCQ	$0, R8

  2288. 

  2289. 	MOVQ	P751P1_8, AX

  2290. 	MULQ	CX

  2291. 	ADDQ	AX, R9

  2292. 	ADCQ	DX, R10

  2293. 	ADCQ	$0, R8

  2294. 	ADDQ	(152)(REG_P1), R9

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

  2296. 	ADCQ	$0, R10

  2297. 	ADCQ	$0, R8

  2298. 

  2299. 	XORQ	R9, R9

  2300. 	MOVQ	P751P1_11, AX

  2301. 	MULQ	R14

  2302. 	ADDQ	AX, R10

  2303. 	ADCQ	DX, R8

  2304. 	ADCQ	$0, R9

  2305. 

  2306. 	MOVQ	P751P1_10, AX

  2307. 	MULQ	R15

  2308. 	ADDQ	AX, R10

  2309. 	ADCQ	DX, R8

  2310. 	ADCQ	$0, R9

  2311. 

  2312. 	MOVQ	P751P1_9, AX

  2313. 	MULQ	CX

  2314. 	ADDQ	AX, R10

  2315. 	ADCQ	DX, R8

  2316. 	ADCQ	$0, R9

  2317. 	ADDQ	(160)(REG_P1), R10

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

  2319. 	ADCQ	$0, R8

  2320. 	ADCQ	$0, R9

  2321. 

  2322. 	XORQ	R10, R10

  2323. 	MOVQ	P751P1_11, AX

  2324. 	MULQ	R15

  2325. 	ADDQ	AX, R8

  2326. 	ADCQ	DX, R9

  2327. 	ADCQ	$0, R10

  2328. 

  2329. 	MOVQ	P751P1_10, AX

  2330. 	MULQ	CX

  2331. 	ADDQ	AX, R8

  2332. 	ADCQ	DX, R9

  2333. 	ADCQ	$0, R10

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

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

  2336. 	ADCQ	$0, R9

  2337. 	ADCQ	$0, R10

  2338. 

  2339. 	MOVQ	P751P1_11, AX

  2340. 	MULQ	CX

  2341. 	ADDQ	AX, R9

  2342. 	ADCQ	DX, R10

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

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

  2345. 	ADCQ	$0, R10

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

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

  2348. 	RET

  2349. 

  2350. redc_with_mulx_adcx_adox:

  2351. 	// This implements the Montgomery reduction algorithm described in

  2352. 	// section 5.2.3 of https://eprint.iacr.org/2017/1015.pdf.

  2353. 	// This assumes that the BMI2 and ADX instruction set extensions are available.

  2354. 	REDC(0(REG_P2), 0(REG_P1), mul256x448bmi2adx)

  2355. 	RET

  2356. 

  2357. redc_with_mulx:

  2358. 	// This implements the Montgomery reduction algorithm described in

  2359. 	// section 5.2.3 of https://eprint.iacr.org/2017/1015.pdf.

  2360. 	// This assumes that the BMI2 instruction set extension is available.

  2361. 	REDC(0(REG_P2), 0(REG_P1), mul256x448bmi2)

  2362. 	RET

  2363. 

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

  2365. 

  2366. 	MOVQ z+0(FP), REG_P3

  2367. 	MOVQ x+8(FP), REG_P1

  2368. 	MOVQ y+16(FP), REG_P2

  2369. 

  2370. 	MOVQ	(REG_P1), R8

  2371. 	MOVQ	(8)(REG_P1), R9

  2372. 	MOVQ	(16)(REG_P1), R10

  2373. 	MOVQ	(24)(REG_P1), R11

  2374. 	MOVQ	(32)(REG_P1), R12

  2375. 	MOVQ	(40)(REG_P1), R13

  2376. 	MOVQ	(48)(REG_P1), R14

  2377. 	MOVQ	(56)(REG_P1), R15

  2378. 	MOVQ	(64)(REG_P1), AX

  2379. 	MOVQ	(72)(REG_P1), BX

  2380. 	MOVQ	(80)(REG_P1), CX

  2381. 	MOVQ	(88)(REG_P1), DI

  2382. 

  2383. 	ADDQ	(REG_P2), R8

  2384. 	ADCQ	(8)(REG_P2), R9

  2385. 	ADCQ	(16)(REG_P2), R10

  2386. 	ADCQ	(24)(REG_P2), R11

  2387. 	ADCQ	(32)(REG_P2), R12

  2388. 	ADCQ	(40)(REG_P2), R13

  2389. 	ADCQ	(48)(REG_P2), R14

  2390. 	ADCQ	(56)(REG_P2), R15

  2391. 	ADCQ	(64)(REG_P2), AX

  2392. 	ADCQ	(72)(REG_P2), BX

  2393. 	ADCQ	(80)(REG_P2), CX

  2394. 	ADCQ	(88)(REG_P2), DI

  2395. 

  2396. 	MOVQ	R8, (REG_P3)

  2397. 	MOVQ	R9, (8)(REG_P3)

  2398. 	MOVQ	R10, (16)(REG_P3)

  2399. 	MOVQ	R11, (24)(REG_P3)

  2400. 	MOVQ	R12, (32)(REG_P3)

  2401. 	MOVQ	R13, (40)(REG_P3)

  2402. 	MOVQ	R14, (48)(REG_P3)

  2403. 	MOVQ	R15, (56)(REG_P3)

  2404. 	MOVQ	AX, (64)(REG_P3)

  2405. 	MOVQ	BX, (72)(REG_P3)

  2406. 	MOVQ	CX, (80)(REG_P3)

  2407. 	MOVQ	DI, (88)(REG_P3)

  2408. 

  2409. 	RET

  2410. 

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

  2412. 

  2413. 	MOVQ z+0(FP), REG_P3

  2414. 	MOVQ x+8(FP), REG_P1

  2415. 	MOVQ y+16(FP), REG_P2

  2416. 

  2417. 	MOVQ	(REG_P1), R8

  2418. 	MOVQ	(8)(REG_P1), R9

  2419. 	MOVQ	(16)(REG_P1), R10

  2420. 	MOVQ	(24)(REG_P1), R11

  2421. 	MOVQ	(32)(REG_P1), R12

  2422. 	MOVQ	(40)(REG_P1), R13

  2423. 	MOVQ	(48)(REG_P1), R14

  2424. 	MOVQ	(56)(REG_P1), R15

  2425. 	MOVQ	(64)(REG_P1), AX

  2426. 	MOVQ	(72)(REG_P1), BX

  2427. 	MOVQ	(80)(REG_P1), CX

  2428. 

  2429. 	ADDQ	(REG_P2), R8

  2430. 	ADCQ	(8)(REG_P2), R9

  2431. 	ADCQ	(16)(REG_P2), R10

  2432. 	ADCQ	(24)(REG_P2), R11

  2433. 	ADCQ	(32)(REG_P2), R12

  2434. 	ADCQ	(40)(REG_P2), R13

  2435. 	ADCQ	(48)(REG_P2), R14

  2436. 	ADCQ	(56)(REG_P2), R15

  2437. 	ADCQ	(64)(REG_P2), AX

  2438. 	ADCQ	(72)(REG_P2), BX

  2439. 	ADCQ	(80)(REG_P2), CX

  2440. 

  2441. 	MOVQ	R8, (REG_P3)

  2442. 	MOVQ	R9, (8)(REG_P3)

  2443. 	MOVQ	R10, (16)(REG_P3)

  2444. 	MOVQ	R11, (24)(REG_P3)

  2445. 	MOVQ	R12, (32)(REG_P3)

  2446. 	MOVQ	R13, (40)(REG_P3)

  2447. 	MOVQ	R14, (48)(REG_P3)

  2448. 	MOVQ	R15, (56)(REG_P3)

  2449. 	MOVQ	AX, (64)(REG_P3)

  2450. 	MOVQ	BX, (72)(REG_P3)

  2451. 	MOVQ	CX, (80)(REG_P3)

  2452. 	MOVQ	(88)(REG_P1), AX

  2453. 	ADCQ	(88)(REG_P2), AX

  2454. 	MOVQ	AX, (88)(REG_P3)

  2455. 

  2456. 	MOVQ	(96)(REG_P1), R8

  2457. 	MOVQ	(104)(REG_P1), R9

  2458. 	MOVQ	(112)(REG_P1), R10

  2459. 	MOVQ	(120)(REG_P1), R11

  2460. 	MOVQ	(128)(REG_P1), R12

  2461. 	MOVQ	(136)(REG_P1), R13

  2462. 	MOVQ	(144)(REG_P1), R14

  2463. 	MOVQ	(152)(REG_P1), R15

  2464. 	MOVQ	(160)(REG_P1), AX

  2465. 	MOVQ	(168)(REG_P1), BX

  2466. 	MOVQ	(176)(REG_P1), CX

  2467. 	MOVQ	(184)(REG_P1), DI

  2468. 

  2469. 	ADCQ	(96)(REG_P2), R8

  2470. 	ADCQ	(104)(REG_P2), R9

  2471. 	ADCQ	(112)(REG_P2), R10

  2472. 	ADCQ	(120)(REG_P2), R11

  2473. 	ADCQ	(128)(REG_P2), R12

  2474. 	ADCQ	(136)(REG_P2), R13

  2475. 	ADCQ	(144)(REG_P2), R14

  2476. 	ADCQ	(152)(REG_P2), R15

  2477. 	ADCQ	(160)(REG_P2), AX

  2478. 	ADCQ	(168)(REG_P2), BX

  2479. 	ADCQ	(176)(REG_P2), CX

  2480. 	ADCQ	(184)(REG_P2), DI

  2481. 

  2482. 	MOVQ	R8, (96)(REG_P3)

  2483. 	MOVQ	R9, (104)(REG_P3)

  2484. 	MOVQ	R10, (112)(REG_P3)

  2485. 	MOVQ	R11, (120)(REG_P3)

  2486. 	MOVQ	R12, (128)(REG_P3)

  2487. 	MOVQ	R13, (136)(REG_P3)

  2488. 	MOVQ	R14, (144)(REG_P3)

  2489. 	MOVQ	R15, (152)(REG_P3)

  2490. 	MOVQ	AX, (160)(REG_P3)

  2491. 	MOVQ	BX, (168)(REG_P3)

  2492. 	MOVQ	CX, (176)(REG_P3)

  2493. 	MOVQ	DI, (184)(REG_P3)

  2494. 

  2495. 	RET

  2496. 

  2497. 

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

  2499. 

  2500. 	MOVQ z+0(FP), REG_P3

  2501. 	MOVQ x+8(FP), REG_P1

  2502. 	MOVQ y+16(FP), REG_P2

  2503. 

  2504. 	MOVQ	(REG_P1), R8

  2505. 	MOVQ	(8)(REG_P1), R9

  2506. 	MOVQ	(16)(REG_P1), R10

  2507. 	MOVQ	(24)(REG_P1), R11

  2508. 	MOVQ	(32)(REG_P1), R12

  2509. 	MOVQ	(40)(REG_P1), R13

  2510. 	MOVQ	(48)(REG_P1), R14

  2511. 	MOVQ	(56)(REG_P1), R15

  2512. 	MOVQ	(64)(REG_P1), AX

  2513. 	MOVQ	(72)(REG_P1), BX

  2514. 	MOVQ	(80)(REG_P1), CX

  2515. 

  2516. 	SUBQ	(REG_P2), R8

  2517. 	SBBQ	(8)(REG_P2), R9

  2518. 	SBBQ	(16)(REG_P2), R10

  2519. 	SBBQ	(24)(REG_P2), R11

  2520. 	SBBQ	(32)(REG_P2), R12

  2521. 	SBBQ	(40)(REG_P2), R13

  2522. 	SBBQ	(48)(REG_P2), R14

  2523. 	SBBQ	(56)(REG_P2), R15

  2524. 	SBBQ	(64)(REG_P2), AX

  2525. 	SBBQ	(72)(REG_P2), BX

  2526. 	SBBQ	(80)(REG_P2), CX

  2527. 

  2528. 	MOVQ	R8, (REG_P3)

  2529. 	MOVQ	R9, (8)(REG_P3)

  2530. 	MOVQ	R10, (16)(REG_P3)

  2531. 	MOVQ	R11, (24)(REG_P3)

  2532. 	MOVQ	R12, (32)(REG_P3)

  2533. 	MOVQ	R13, (40)(REG_P3)

  2534. 	MOVQ	R14, (48)(REG_P3)

  2535. 	MOVQ	R15, (56)(REG_P3)

  2536. 	MOVQ	AX, (64)(REG_P3)

  2537. 	MOVQ	BX, (72)(REG_P3)

  2538. 	MOVQ	CX, (80)(REG_P3)

  2539. 	MOVQ	(88)(REG_P1), AX

  2540. 	SBBQ	(88)(REG_P2), AX

  2541. 	MOVQ	AX, (88)(REG_P3)

  2542. 

  2543. 	MOVQ	(96)(REG_P1), R8

  2544. 	MOVQ	(104)(REG_P1), R9

  2545. 	MOVQ	(112)(REG_P1), R10

  2546. 	MOVQ	(120)(REG_P1), R11

  2547. 	MOVQ	(128)(REG_P1), R12

  2548. 	MOVQ	(136)(REG_P1), R13

  2549. 	MOVQ	(144)(REG_P1), R14

  2550. 	MOVQ	(152)(REG_P1), R15

  2551. 	MOVQ	(160)(REG_P1), AX

  2552. 	MOVQ	(168)(REG_P1), BX

  2553. 	MOVQ	(176)(REG_P1), CX

  2554. 	MOVQ	(184)(REG_P1), DI

  2555. 

  2556. 	SBBQ	(96)(REG_P2), R8

  2557. 	SBBQ	(104)(REG_P2), R9

  2558. 	SBBQ	(112)(REG_P2), R10

  2559. 	SBBQ	(120)(REG_P2), R11

  2560. 	SBBQ	(128)(REG_P2), R12

  2561. 	SBBQ	(136)(REG_P2), R13

  2562. 	SBBQ	(144)(REG_P2), R14

  2563. 	SBBQ	(152)(REG_P2), R15

  2564. 	SBBQ	(160)(REG_P2), AX

  2565. 	SBBQ	(168)(REG_P2), BX

  2566. 	SBBQ	(176)(REG_P2), CX

  2567. 	SBBQ	(184)(REG_P2), DI

  2568. 

  2569. 	MOVQ	R8, (96)(REG_P3)

  2570. 	MOVQ	R9, (104)(REG_P3)

  2571. 	MOVQ	R10, (112)(REG_P3)

  2572. 	MOVQ	R11, (120)(REG_P3)

  2573. 	MOVQ	R12, (128)(REG_P3)

  2574. 	MOVQ	R13, (136)(REG_P3)

  2575. 	MOVQ	R14, (144)(REG_P3)

  2576. 	MOVQ	R15, (152)(REG_P3)

  2577. 	MOVQ	AX, (160)(REG_P3)

  2578. 	MOVQ	BX, (168)(REG_P3)

  2579. 	MOVQ	CX, (176)(REG_P3)

  2580. 	MOVQ	DI, (184)(REG_P3)

  2581. 

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

  2583. 	MOVQ	$0, AX

  2584. 	SBBQ	$0, AX

  2585. 

  2586. 	// Load p into registers:

  2587. 	MOVQ	P751_0, R8

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

  2589. 	MOVQ	P751_5, R9

  2590. 	MOVQ	P751_6, R10

  2591. 	MOVQ	P751_7, R11

  2592. 	MOVQ	P751_8, R12

  2593. 	MOVQ	P751_9, R13

  2594. 	MOVQ	P751_10, R14

  2595. 	MOVQ	P751_11, R15

  2596. 

  2597. 	ANDQ	AX, R8

  2598. 	ANDQ	AX, R9

  2599. 	ANDQ	AX, R10

  2600. 	ANDQ	AX, R11

  2601. 	ANDQ	AX, R12

  2602. 	ANDQ	AX, R13

  2603. 	ANDQ	AX, R14

  2604. 	ANDQ	AX, R15

  2605. 

  2606. 	ADDQ	R8,  (96   )(REG_P3)

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

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

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

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

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

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

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

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

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

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

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

  2618. 

  2619. 	RET