diff --git a/src/build.json b/src/build.json
index f8948fb..2372b50 100644
--- a/src/build.json
+++ b/src/build.json
@@ -93,6 +93,10 @@
             "crypto/fipsmodule/sha/sha512.c",
             "crypto/fipsmodule/tls/kdf.c"
         ],
+        "asm": [
+            "third_party/fiat/asm/fiat_p256_adx_mul.S",
+            "third_party/fiat/asm/fiat_p256_adx_sqr.S"
+        ],
         "perlasm_aarch64": [
             {"src": "crypto/fipsmodule/aes/asm/aesv8-armx.pl", "dst": "aesv8-armv8"},
             {"src": "crypto/fipsmodule/modes/asm/aesv8-gcm-armv8.pl"},
@@ -548,9 +552,7 @@
             "crypto/hrss/asm/poly_rq_mul.S",
             "crypto/poly1305/poly1305_arm_asm.S",
             "third_party/fiat/asm/fiat_curve25519_adx_mul.S",
-            "third_party/fiat/asm/fiat_curve25519_adx_square.S",
-            "third_party/fiat/asm/fiat_p256_adx_mul.S",
-            "third_party/fiat/asm/fiat_p256_adx_sqr.S"
+            "third_party/fiat/asm/fiat_curve25519_adx_square.S"
         ],
         "perlasm_aarch64": [
             {"src": "crypto/chacha/asm/chacha-armv8.pl"},
diff --git a/src/gen/sources.bzl b/src/gen/sources.bzl
index 6903427..b162a45 100644
--- a/src/gen/sources.bzl
+++ b/src/gen/sources.bzl
@@ -195,6 +195,8 @@
   "gen/bcm/x86_64-mont-linux.S",
   "gen/bcm/x86_64-mont5-apple.S",
   "gen/bcm/x86_64-mont5-linux.S",
+  "third_party/fiat/asm/fiat_p256_adx_mul.S",
+  "third_party/fiat/asm/fiat_p256_adx_sqr.S",
 ]
 
 bcm_sources_nasm = [
@@ -666,8 +668,6 @@
   "gen/crypto/chacha20_poly1305_x86_64-linux.S",
   "third_party/fiat/asm/fiat_curve25519_adx_mul.S",
   "third_party/fiat/asm/fiat_curve25519_adx_square.S",
-  "third_party/fiat/asm/fiat_p256_adx_mul.S",
-  "third_party/fiat/asm/fiat_p256_adx_sqr.S",
 ]
 
 crypto_sources_nasm = [
diff --git a/src/gen/sources.cmake b/src/gen/sources.cmake
index d7e1e74..91c2395 100644
--- a/src/gen/sources.cmake
+++ b/src/gen/sources.cmake
@@ -201,6 +201,8 @@
   gen/bcm/x86_64-mont-linux.S
   gen/bcm/x86_64-mont5-apple.S
   gen/bcm/x86_64-mont5-linux.S
+  third_party/fiat/asm/fiat_p256_adx_mul.S
+  third_party/fiat/asm/fiat_p256_adx_sqr.S
 )
 
 set(
@@ -686,8 +688,6 @@
   gen/crypto/chacha20_poly1305_x86_64-linux.S
   third_party/fiat/asm/fiat_curve25519_adx_mul.S
   third_party/fiat/asm/fiat_curve25519_adx_square.S
-  third_party/fiat/asm/fiat_p256_adx_mul.S
-  third_party/fiat/asm/fiat_p256_adx_sqr.S
 )
 
 set(
diff --git a/src/gen/sources.json b/src/gen/sources.json
index 5d96a60..e6cc5db 100644
--- a/src/gen/sources.json
+++ b/src/gen/sources.json
@@ -178,7 +178,9 @@
       "gen/bcm/x86_64-mont-apple.S",
       "gen/bcm/x86_64-mont-linux.S",
       "gen/bcm/x86_64-mont5-apple.S",
-      "gen/bcm/x86_64-mont5-linux.S"
+      "gen/bcm/x86_64-mont5-linux.S",
+      "third_party/fiat/asm/fiat_p256_adx_mul.S",
+      "third_party/fiat/asm/fiat_p256_adx_sqr.S"
     ],
     "nasm": [
       "gen/bcm/aesni-gcm-x86_64-win.asm",
@@ -646,9 +648,7 @@
       "gen/crypto/chacha20_poly1305_x86_64-apple.S",
       "gen/crypto/chacha20_poly1305_x86_64-linux.S",
       "third_party/fiat/asm/fiat_curve25519_adx_mul.S",
-      "third_party/fiat/asm/fiat_curve25519_adx_square.S",
-      "third_party/fiat/asm/fiat_p256_adx_mul.S",
-      "third_party/fiat/asm/fiat_p256_adx_sqr.S"
+      "third_party/fiat/asm/fiat_curve25519_adx_square.S"
     ],
     "nasm": [
       "gen/crypto/aes128gcmsiv-x86_64-win.asm",
diff --git a/src/third_party/fiat/asm/fiat_p256_adx_mul.S b/src/third_party/fiat/asm/fiat_p256_adx_mul.S
index d7ebd21..c4010b3 100644
--- a/src/third_party/fiat/asm/fiat_p256_adx_mul.S
+++ b/src/third_party/fiat/asm/fiat_p256_adx_mul.S
@@ -3,7 +3,6 @@
 #if !defined(OPENSSL_NO_ASM) && defined(OPENSSL_X86_64) && \
     (defined(__APPLE__) || defined(__ELF__))
 
-.intel_syntax noprefix
 .text
 #if defined(__APPLE__)
 .private_extern _fiat_p256_adx_mul
@@ -18,158 +17,158 @@
 
 .cfi_startproc
 _CET_ENDBR
-push rbp
-.cfi_adjust_cfa_offset 8
+pushq %rbp
+;.cfi_adjust_cfa_offset 8
 .cfi_offset rbp, -16
-mov rbp, rsp
-mov rax, rdx
-mov rdx, [ rsi + 0x0 ]
-test al, al
-mulx r8, rcx, [ rax + 0x0 ]
-mov [ rsp - 0x80 ], rbx
+movq %rsp, %rbp
+movq %rdx, %rax
+movq (%rsi), %rdx
+testb %al, %al
+mulxq (%rax), %rcx, %r8
+movq %rbx, -0x80(%rsp)
 .cfi_offset rbx, -16-0x80
-mulx rbx, r9, [ rax + 0x8 ]
-mov [ rsp - 0x68 ], r14
+mulxq 0x8(%rax), %r9, %rbx
+movq %r14, -0x68(%rsp)
 .cfi_offset r14, -16-0x68
-adc r9, r8
-mov [ rsp - 0x60 ], r15
+adcq %r8, %r9
+movq %r15, -0x60(%rsp)
 .cfi_offset r15, -16-0x60
-mulx r15, r14, [ rax + 0x10 ]
-mov [ rsp - 0x78 ], r12
+mulxq 0x10(%rax), %r14, %r15
+movq %r12, -0x78(%rsp)
 .cfi_offset r12, -16-0x78
-adc r14, rbx
-mulx r11, r10, [ rax + 0x18 ]
-mov [ rsp - 0x70 ], r13
+adcq %rbx, %r14
+mulxq 0x18(%rax), %r10, %r11
+movq %r13, -0x70(%rsp)
 .cfi_offset r13, -16-0x70
-adc r10, r15
-mov rdx, [ rsi + 0x8 ]
-mulx rbx, r8, [ rax + 0x0 ]
-adc r11, 0x0
-xor r15, r15
-adcx r8, r9
-adox rbx, r14
-mov [ rsp - 0x58 ], rdi
-mulx rdi, r9, [ rax + 0x8 ]
-adcx r9, rbx
-adox rdi, r10
-mulx rbx, r14, [ rax + 0x10 ]
-adcx r14, rdi
-adox rbx, r11
-mulx r13, r12, [ rax + 0x18 ]
-adcx r12, rbx
-mov rdx, 0x100000000
-mulx r11, r10, rcx
-adox r13, r15
-adcx r13, r15
-xor rdi, rdi
-adox r10, r8
-mulx r8, rbx, r10
-adox r11, r9
-adcx rbx, r11
-adox r8, r14
-mov rdx, 0xffffffff00000001
-mulx r9, r15, rcx
-adcx r15, r8
-adox r9, r12
-mulx r14, rcx, r10
-mov rdx, [ rsi + 0x10 ]
-mulx r10, r12, [ rax + 0x8 ]
-adcx rcx, r9
-adox r14, r13
-mulx r11, r13, [ rax + 0x0 ]
-mov r9, rdi
-adcx r14, r9
-adox rdi, rdi
-adc rdi, 0x0
-xor r9, r9
-adcx r13, rbx
-adox r11, r15
-mov rdx, [ rsi + 0x10 ]
-mulx r15, r8, [ rax + 0x10 ]
-adox r10, rcx
-mulx rcx, rbx, [ rax + 0x18 ]
-mov rdx, [ rsi + 0x18 ]
-adcx r12, r11
-mulx rsi, r11, [ rax + 0x8 ]
-adcx r8, r10
-adox r15, r14
-adcx rbx, r15
-adox rcx, r9
-adcx rcx, r9
-mulx r15, r10, [ rax + 0x0 ]
-add rcx, rdi
-mov r14, r9
-adc r14, 0
-xor r9, r9
-adcx r10, r12
-adox r15, r8
-adcx r11, r15
-adox rsi, rbx
-mulx r8, r12, [ rax + 0x10 ]
-adox r8, rcx
-mulx rcx, rbx, [ rax + 0x18 ]
-adcx r12, rsi
-adox rcx, r9
-mov rdx, 0x100000000
-adcx rbx, r8
-adc rcx, 0
-mulx rdi, r15, r13
-xor rax, rax
-adcx rcx, r14
-adc rax, 0
-xor r9, r9
-adox r15, r10
-mulx r14, r10, r15
-adox rdi, r11
-mov rdx, 0xffffffff00000001
-adox r14, r12
-adcx r10, rdi
-mulx r12, r11, r13
-adcx r11, r14
-adox r12, rbx
-mulx rbx, r13, r15
-adcx r13, r12
-adox rbx, rcx
-mov r8, r9
-adox rax, r9
-adcx r8, rbx
-adc rax, 0x0
-mov rcx, rax
-mov r15, 0xffffffffffffffff
-mov rdi, r10
-sub rdi, r15
-mov r14, 0xffffffff
-mov r12, r11
-sbb r12, r14
-mov rbx, r13
-sbb rbx, r9
-mov rax, rax
-mov rax, r8
-sbb rax, rdx
-sbb rcx, r9
-cmovc rdi, r10
-mov r10, [ rsp - 0x58 ]
-cmovc rbx, r13
-mov r13, [ rsp - 0x70 ]
+adcq %r15, %r10
+movq 0x8(%rsi), %rdx
+mulxq (%rax), %r8, %rbx
+adcq $0x0, %r11
+xorq %r15, %r15
+adcxq %r9, %r8
+adoxq %r14, %rbx
+movq %rdi, -0x58(%rsp)
+mulxq 0x8(%rax), %r9, %rdi
+adcxq %rbx, %r9
+adoxq %r10, %rdi
+mulxq 0x10(%rax), %r14, %rbx
+adcxq %rdi, %r14
+adoxq %r11, %rbx
+mulxq 0x18(%rax), %r12, %r13
+adcxq %rbx, %r12
+movq $0x100000000, %rdx
+mulxq %rcx, %r10, %r11
+adoxq %r15, %r13
+adcxq %r15, %r13
+xorq %rdi, %rdi
+adoxq %r8, %r10
+mulxq %r10, %rbx, %r8
+adoxq %r9, %r11
+adcxq %r11, %rbx
+adoxq %r14, %r8
+movq $0xffffffff00000001, %rdx
+mulxq %rcx, %r15, %r9
+adcxq %r8, %r15
+adoxq %r12, %r9
+mulxq %r10, %rcx, %r14
+movq 0x10(%rsi), %rdx
+mulxq 0x8(%rax), %r12, %r10
+adcxq %r9, %rcx
+adoxq %r13, %r14
+mulxq (%rax), %r13, %r11
+movq %rdi, %r9
+adcxq %r9, %r14
+adoxq %rdi, %rdi
+adcq $0x0, %rdi
+xorq %r9, %r9
+adcxq %rbx, %r13
+adoxq %r15, %r11
+movq 0x10(%rsi), %rdx
+mulxq 0x10(%rax), %r8, %r15
+adoxq %rcx, %r10
+mulxq 0x18(%rax), %rbx, %rcx
+movq 0x18(%rsi), %rdx
+adcxq %r11, %r12
+mulxq 0x8(%rax), %r11, %rsi
+adcxq %r10, %r8
+adoxq %r14, %r15
+adcxq %r15, %rbx
+adoxq %r9, %rcx
+adcxq %r9, %rcx
+mulxq (%rax), %r10, %r15
+addq %rdi, %rcx
+movq %r9, %r14
+adcq $0x0, %r14
+xorq %r9, %r9
+adcxq %r12, %r10
+adoxq %r8, %r15
+adcxq %r15, %r11
+adoxq %rbx, %rsi
+mulxq 0x10(%rax), %r12, %r8
+adoxq %rcx, %r8
+mulxq 0x18(%rax), %rbx, %rcx
+adcxq %rsi, %r12
+adoxq %r9, %rcx
+movq $0x100000000, %rdx
+adcxq %r8, %rbx
+adcq $0x0, %rcx
+mulxq %r13, %r15, %rdi
+xorq %rax, %rax
+adcxq %r14, %rcx
+adcq $0x0, %rax
+xorq %r9, %r9
+adoxq %r10, %r15
+mulxq %r15, %r10, %r14
+adoxq %r11, %rdi
+movq $0xffffffff00000001, %rdx
+adoxq %r12, %r14
+adcxq %rdi, %r10
+mulxq %r13, %r11, %r12
+adcxq %r14, %r11
+adoxq %rbx, %r12
+mulxq %r15, %r13, %rbx
+adcxq %r12, %r13
+adoxq %rcx, %rbx
+movq %r9, %r8
+adoxq %r9, %rax
+adcxq %rbx, %r8
+adcq $0x0, %rax
+movq %rax, %rcx
+movq $0xffffffffffffffff, %r15
+movq %r10, %rdi
+subq %r15, %rdi
+movq $0xffffffff, %r14
+movq %r11, %r12
+sbbq %r14, %r12
+movq %r13, %rbx
+sbbq %r9, %rbx
+movq %rax, %rax
+movq %r8, %rax
+sbbq %rdx, %rax
+sbbq %r9, %rcx
+cmovcq %r10, %rdi
+movq -0x58(%rsp), %r10
+cmovcq %r13, %rbx
+movq -0x70(%rsp), %r13
 .cfi_restore r13
-cmovc r12, r11
-cmovc rax, r8
-mov [ r10 + 0x10 ], rbx
-mov rbx, [ rsp - 0x80 ]
+cmovcq %r11, %r12
+cmovcq %r8, %rax
+movq %rbx, 0x10(%r10)
+movq -0x80(%rsp), %rbx
 .cfi_restore rbx
-mov [ r10 + 0x0 ], rdi
-mov [ r10 + 0x8 ], r12
-mov [ r10 + 0x18 ], rax
-mov r12, [ rsp - 0x78 ]
+movq %rdi, (%r10)
+movq %r12, 0x8(%r10)
+movq %rax, 0x18(%r10)
+movq -0x78(%rsp), %r12
 .cfi_restore r12
-mov r14, [ rsp - 0x68 ]
+movq -0x68(%rsp), %r14
 .cfi_restore r14
-mov r15, [ rsp - 0x60 ]
+movq -0x60(%rsp), %r15
 .cfi_restore r15
-pop rbp
+popq %rbp
 .cfi_restore rbp
 .cfi_adjust_cfa_offset -8
-ret
+retq
 .cfi_endproc
 #if defined(__ELF__)
 .size fiat_p256_adx_mul, .-fiat_p256_adx_mul
diff --git a/src/third_party/fiat/asm/fiat_p256_adx_sqr.S b/src/third_party/fiat/asm/fiat_p256_adx_sqr.S
index cca269f..c4dea91 100644
--- a/src/third_party/fiat/asm/fiat_p256_adx_sqr.S
+++ b/src/third_party/fiat/asm/fiat_p256_adx_sqr.S
@@ -3,7 +3,6 @@
 #if !defined(OPENSSL_NO_ASM) && defined(OPENSSL_X86_64) && \
     (defined(__APPLE__) || defined(__ELF__))
 
-.intel_syntax noprefix
 .text
 #if defined(__APPLE__)
 .private_extern _fiat_p256_adx_sqr
@@ -18,147 +17,147 @@
 
 .cfi_startproc
 _CET_ENDBR
-push rbp
+pushq %rbp
 .cfi_adjust_cfa_offset 8
 .cfi_offset rbp, -16
-mov rbp, rsp
-mov rdx, [ rsi + 0x0 ]
-mulx r10, rax, [ rsi + 0x18 ]
-mulx rcx, r11, rdx
-mulx r9, r8, [ rsi + 0x8 ]
-mov [ rsp - 0x80 ], rbx
+movq %rsp, %rbp
+movq (%rsi), %rdx
+mulxq 0x18(%rsi), %rax, %r10
+mulxq %rdx, %r11, %rcx
+mulxq 0x8(%rsi), %r8, %r9
+movq %rbx, -0x80(%rsp)
 .cfi_offset rbx, -16-0x80
-xor rbx, rbx
-adox r8, r8
-mov [ rsp - 0x78 ], r12
+xorq %rbx, %rbx
+adoxq %r8, %r8
+movq %r12, -0x78(%rsp)
 .cfi_offset r12, -16-0x78
-mulx r12, rbx, [ rsi + 0x10 ]
-mov rdx, [ rsi + 0x8 ]
-mov [ rsp - 0x70 ], r13
+mulxq 0x10(%rsi), %rbx, %r12
+movq 0x8(%rsi), %rdx
+movq %r13, -0x70(%rsp)
 .cfi_offset r13, -16-0x70
-mov [ rsp - 0x68 ], r14
+movq %r14, -0x68(%rsp)
 .cfi_offset r14, -16-0x68
-mulx r14, r13, rdx
-mov [ rsp - 0x60 ], r15
+mulxq %rdx, %r13, %r14
+movq %r15, -0x60(%rsp)
 .cfi_offset r15, -16-0x60
-mov [ rsp - 0x58 ], rdi
-mulx rdi, r15, [ rsi + 0x10 ]
-adcx r12, r15
-mov [ rsp - 0x50 ], r11
-mulx r11, r15, [ rsi + 0x18 ]
-adcx r10, rdi
-mov rdi, 0x0
-adcx r11, rdi
+movq %rdi, -0x58(%rsp)
+mulxq 0x10(%rsi), %r15, %rdi
+adcxq %r15, %r12
+movq %r11, -0x50(%rsp)
+mulxq 0x18(%rsi), %r15, %r11
+adcxq %rdi, %r10
+movq $0x0, %rdi
+adcxq %rdi, %r11
 clc
-adcx rbx, r9
-adox rbx, rbx
-adcx rax, r12
-adox rax, rax
-adcx r15, r10
-adox r15, r15
-mov rdx, [ rsi + 0x10 ]
-mulx r12, r9, [ rsi + 0x18 ]
-adcx r9, r11
-adcx r12, rdi
-mulx r11, r10, rdx
+adcxq %r9, %rbx
+adoxq %rbx, %rbx
+adcxq %r12, %rax
+adoxq %rax, %rax
+adcxq %r10, %r15
+adoxq %r15, %r15
+movq 0x10(%rsi), %rdx
+mulxq 0x18(%rsi), %r9, %r12
+adcxq %r11, %r9
+adcxq %rdi, %r12
+mulxq %rdx, %r10, %r11
 clc
-adcx rcx, r8
-adcx r13, rbx
-adcx r14, rax
-adox r9, r9
-adcx r10, r15
-mov rdx, [ rsi + 0x18 ]
-mulx rbx, r8, rdx
-adox r12, r12
-adcx r11, r9
-mov rsi, [ rsp - 0x50 ]
-adcx r8, r12
-mov rax, 0x100000000
-mov rdx, rax
-mulx r15, rax, rsi
-adcx rbx, rdi
-adox rbx, rdi
-xor r9, r9
-adox rax, rcx
-adox r15, r13
-mulx rcx, rdi, rax
-adcx rdi, r15
-adox rcx, r14
-mov rdx, 0xffffffff00000001
-mulx r14, r13, rsi
-adox r14, r10
-adcx r13, rcx
-mulx r12, r10, rax
-adox r12, r11
-mov r11, r9
-adox r11, r8
-adcx r10, r14
-mov r8, r9
-adcx r8, r12
-mov rax, r9
-adcx rax, r11
-mov r15, r9
-adox r15, rbx
-mov rdx, 0x100000000
-mulx rcx, rbx, rdi
-mov r14, r9
-adcx r14, r15
-mov r12, r9
-adox r12, r12
-adcx r12, r9
-adox rbx, r13
-mulx r11, r13, rbx
-mov r15, 0xffffffff00000001
-mov rdx, r15
-mulx rsi, r15, rbx
-adox rcx, r10
-adox r11, r8
-mulx r8, r10, rdi
-adcx r13, rcx
-adox r8, rax
-adcx r10, r11
-adox rsi, r14
-mov rdi, r12
-mov rax, r9
-adox rdi, rax
-adcx r15, r8
-mov r14, rax
-adcx r14, rsi
-adcx rdi, r9
-dec r9
-mov rbx, r13
-sub rbx, r9
-mov rcx, 0xffffffff
-mov r11, r10
-sbb r11, rcx
-mov r8, r15
-sbb r8, rax
-mov rsi, r14
-sbb rsi, rdx
-sbb rdi, rax
-cmovc rbx, r13
-cmovc r8, r15
-cmovc r11, r10
-cmovc rsi, r14
-mov rdi, [ rsp - 0x58 ]
-mov [ rdi + 0x18 ], rsi
-mov [ rdi + 0x0 ], rbx
-mov [ rdi + 0x8 ], r11
-mov [ rdi + 0x10 ], r8
-mov rbx, [ rsp - 0x80 ]
+adcxq %r8, %rcx
+adcxq %rbx, %r13
+adcxq %rax, %r14
+adoxq %r9, %r9
+adcxq %r15, %r10
+movq 0x18(%rsi), %rdx
+mulxq %rdx, %r8, %rbx
+adoxq %r12, %r12
+adcxq %r9, %r11
+movq -0x50(%rsp), %rsi
+adcxq %r12, %r8
+movq $0x100000000, %rax
+movq %rax, %rdx
+mulxq %rsi, %rax, %r15
+adcxq %rdi, %rbx
+adoxq %rdi, %rbx
+xorq %r9, %r9
+adoxq %rcx, %rax
+adoxq %r13, %r15
+mulxq %rax, %rdi, %rcx
+adcxq %r15, %rdi
+adoxq %r14, %rcx
+movq $0xffffffff00000001, %rdx
+mulxq %rsi, %r13, %r14
+adoxq %r10, %r14
+adcxq %rcx, %r13
+mulxq %rax, %r10, %r12
+adoxq %r11, %r12
+movq %r9, %r11
+adoxq %r8, %r11
+adcxq %r14, %r10
+movq %r9, %r8
+adcxq %r12, %r8
+movq %r9, %rax
+adcxq %r11, %rax
+movq %r9, %r15
+adoxq %rbx, %r15
+movq $0x100000000, %rdx
+mulxq %rdi, %rbx, %rcx
+movq %r9, %r14
+adcxq %r15, %r14
+movq %r9, %r12
+adoxq %r12, %r12
+adcxq %r9, %r12
+adoxq %r13, %rbx
+mulxq %rbx, %r13, %r11
+movq $0xffffffff00000001, %r15
+movq %r15, %rdx
+mulxq %rbx, %r15, %rsi
+adoxq %r10, %rcx
+adoxq %r8, %r11
+mulxq %rdi, %r10, %r8
+adcxq %rcx, %r13
+adoxq %rax, %r8
+adcxq %r11, %r10
+adoxq %r14, %rsi
+movq %r12, %rdi
+movq %r9, %rax
+adoxq %rax, %rdi
+adcxq %r8, %r15
+movq %rax, %r14
+adcxq %rsi, %r14
+adcxq %r9, %rdi
+decq %r9
+movq %r13, %rbx
+subq %r9, %rbx
+movq $0xffffffff, %rcx
+movq %r10, %r11
+sbbq %rcx, %r11
+movq %r15, %r8
+sbbq %rax, %r8
+movq %r14, %rsi
+sbbq %rdx, %rsi
+sbbq %rax, %rdi
+cmovcq %r13, %rbx
+cmovcq %r15, %r8
+cmovcq %r10, %r11
+cmovcq %r14, %rsi
+movq -0x58(%rsp), %rdi
+movq %rsi, 0x18(%rdi)
+movq %rbx, (%rdi)
+movq %r11, 0x8(%rdi)
+movq %r8, 0x10(%rdi)
+movq -0x80(%rsp), %rbx
 .cfi_restore rbx
-mov r12, [ rsp - 0x78 ]
+movq -0x78(%rsp), %r12
 .cfi_restore r12
-mov r13, [ rsp - 0x70 ]
+movq -0x70(%rsp), %r13
 .cfi_restore r13
-mov r14, [ rsp - 0x68 ]
+movq -0x68(%rsp), %r14
 .cfi_restore r14
-mov r15, [ rsp - 0x60 ]
+movq -0x60(%rsp), %r15
 .cfi_restore r15
-pop rbp
+popq %rbp
 .cfi_restore rbp
 .cfi_adjust_cfa_offset -8
-ret
+retq
 .cfi_endproc
 #if defined(__ELF__)
 .size fiat_p256_adx_sqr, .-fiat_p256_adx_sqr