Rename keccak_f1600_x4_scalar_v8a_asm_hybrid -> keccak_f1600_x4_scalar_v8a_hybrid_asm

mkannwischer · mkannwischer · commit 6b661c6ffffd · 2025-05-19T17:26:46.000+08:00
Signed-off-by: Matthias J. Kannwischer &lt;matthias@kannwischer.eu&gt;
diff --git a/dev/fips202/aarch64/src/fips202_native_aarch64.h b/dev/fips202/aarch64/src/fips202_native_aarch64.h
@@ -38,9 +38,9 @@ __contract__(
   assigns(memory_slice(state, sizeof(uint64_t) * 25 * 2))
 );
 
-#define mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid \
-  MLK_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid)
-void mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid(uint64_t *state,
+#define mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm \
+  MLK_NAMESPACE(keccak_f1600_x4_scalar_v8a_hybrid_asm)
+void mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm(uint64_t *state,
                                                uint64_t const *rc)
 __contract__(
   requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4))
diff --git a/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_asm.S b/dev/fips202/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_asm.S
@@ -842,9 +842,9 @@
 .endm
 
     .text
-    .global MLK_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid)
+    .global MLK_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_hybrid_asm)
     .balign 4
-MLK_ASM_FN_SYMBOL(keccak_f1600_x4_scalar_v8a_asm_hybrid)
+MLK_ASM_FN_SYMBOL(keccak_f1600_x4_scalar_v8a_hybrid_asm)
     alloc_stack
     save_gprs
     save_vregs
diff --git a/dev/fips202/aarch64/x4_v8a_scalar.h b/dev/fips202/aarch64/x4_v8a_scalar.h
@@ -15,7 +15,7 @@
 #include "src/fips202_native_aarch64.h"
 static MLK_INLINE void mlk_keccak_f1600_x4_native(uint64_t *state)
 {
-  mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid(state,
+  mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm(state,
                                             mlk_keccakf1600_round_constants);
 }
 #endif /* !__ASSEMBLER__ */
diff --git a/dev/fips202/aarch64_symbolic/keccak_f1600_x4_v8a_scalar_hybrid_clean.S b/dev/fips202/aarch64_symbolic/keccak_f1600_x4_v8a_scalar_hybrid_clean.S
@@ -842,9 +842,9 @@
 .endm
 
     .text
-    .global MLK_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid)
+    .global MLK_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_hybrid_asm)
     .balign 4
-MLK_ASM_FN_SYMBOL(keccak_f1600_x4_scalar_v8a_asm_hybrid)
+MLK_ASM_FN_SYMBOL(keccak_f1600_x4_scalar_v8a_hybrid_asm)
     alloc_stack
     save_gprs
     save_vregs
diff --git a/examples/monolithic_build/mlkem_native_monobuild.c b/examples/monolithic_build/mlkem_native_monobuild.c
@@ -376,7 +376,7 @@
 #undef mlk_keccak_f1600_x1_scalar_asm
 #undef mlk_keccak_f1600_x1_v84a_asm
 #undef mlk_keccak_f1600_x2_v84a_asm
-#undef mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid
+#undef mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm
 #undef mlk_keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm
 #undef mlk_keccakf1600_round_constants
 /* mlkem/fips202/native/aarch64/x1_scalar.h */
diff --git a/mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h b/mlkem/fips202/native/aarch64/src/fips202_native_aarch64.h
@@ -38,9 +38,9 @@ __contract__(
   assigns(memory_slice(state, sizeof(uint64_t) * 25 * 2))
 );
 
-#define mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid \
-  MLK_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid)
-void mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid(uint64_t *state,
+#define mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm \
+  MLK_NAMESPACE(keccak_f1600_x4_scalar_v8a_hybrid_asm)
+void mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm(uint64_t *state,
                                                uint64_t const *rc)
 __contract__(
   requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4))
diff --git a/mlkem/fips202/native/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_asm.S b/mlkem/fips202/native/aarch64/src/keccak_f1600_x4_v8a_scalar_hybrid_asm.S
@@ -39,8 +39,8 @@
 
 .text
 .balign 4
-.global MLK_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_asm_hybrid)
-MLK_ASM_FN_SYMBOL(keccak_f1600_x4_scalar_v8a_asm_hybrid)
+.global MLK_ASM_NAMESPACE(keccak_f1600_x4_scalar_v8a_hybrid_asm)
+MLK_ASM_FN_SYMBOL(keccak_f1600_x4_scalar_v8a_hybrid_asm)
 
         sub	sp, sp, #0xe0
         stp	x19, x20, [sp, #0x30]
diff --git a/mlkem/fips202/native/aarch64/x4_v8a_scalar.h b/mlkem/fips202/native/aarch64/x4_v8a_scalar.h
@@ -15,7 +15,7 @@
 #include "src/fips202_native_aarch64.h"
 static MLK_INLINE void mlk_keccak_f1600_x4_native(uint64_t *state)
 {
-  mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid(state,
+  mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm(state,
                                             mlk_keccakf1600_round_constants);
 }
 #endif /* !__ASSEMBLER__ */
diff --git a/proofs/cbmc/keccak_f1600_x4_native_aarch64_scalar_v8a_hybrid/Makefile b/proofs/cbmc/keccak_f1600_x4_native_aarch64_scalar_v8a_hybrid/Makefile
@@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/fips202/native/aarch64/src/keccakf1600_round_constants.c 
 
 CHECK_FUNCTION_CONTRACTS=mlk_keccak_f1600_x4_native
-USE_FUNCTION_CONTRACTS=mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid
+USE_FUNCTION_CONTRACTS=mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
diff --git a/proofs/cbmc/keccak_f1600_x4_native_aarch64_scalar_v8a_v84a_hybrid/Makefile b/proofs/cbmc/keccak_f1600_x4_native_aarch64_scalar_v8a_v84a_hybrid/Makefile
@@ -10,7 +10,7 @@ HARNESS_FILE = keccak_f1600_x4_native_aarch64_scalar_v8a_v84a_hybrid_harness
 # Litani dashboard. It can be human-readable and contain spaces if you wish.
 PROOF_UID = keccak_f1600_x4_native_aarch64_scalar_v8a_v84a_hybrid
 
-DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 -DMLK_CONFIG_FIPS202_BACKEND_FILE="\"$(SRCDIR)/mlkem/fips202/native/aarch64/x4_v8a_v84a_scalar.h\"" -DMLK_CHECK_APIS
+DEFINES += -DMLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 -DMLK_CONFIG_FIPS202_BACKEND_FILE="\"$(SRCDIR)/mlkem/fips202/native/aarch64/x4_v8a_v84a_scalar.h\"" -DMLK_CHECK_APIS -D__ARM_FEATURE_SHA3
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
diff --git a/proofs/hol_light/arm/mlkem/keccak_f1600_x4_v8a_scalar.S b/proofs/hol_light/arm/mlkem/keccak_f1600_x4_v8a_scalar.S
@@ -37,11 +37,11 @@
 .text
 .balign 4
 #ifdef __APPLE__
-.global _PQCP_MLKEM_NATIVE_MLKEM768_keccak_f1600_x4_scalar_v8a_asm_hybrid
-_PQCP_MLKEM_NATIVE_MLKEM768_keccak_f1600_x4_scalar_v8a_asm_hybrid:
+.global _PQCP_MLKEM_NATIVE_MLKEM768_keccak_f1600_x4_scalar_v8a_hybrid_asm
+_PQCP_MLKEM_NATIVE_MLKEM768_keccak_f1600_x4_scalar_v8a_hybrid_asm:
 #else
-.global PQCP_MLKEM_NATIVE_MLKEM768_keccak_f1600_x4_scalar_v8a_asm_hybrid
-PQCP_MLKEM_NATIVE_MLKEM768_keccak_f1600_x4_scalar_v8a_asm_hybrid:
+.global PQCP_MLKEM_NATIVE_MLKEM768_keccak_f1600_x4_scalar_v8a_hybrid_asm
+PQCP_MLKEM_NATIVE_MLKEM768_keccak_f1600_x4_scalar_v8a_hybrid_asm:
 #endif
 
         sub	sp, sp, #0xe0

Original file line number	Diff line number	Diff line change
`@@ -15,7 +15,7 @@`
`15`	`15`	`#include "src/fips202_native_aarch64.h"`
`16`	`16`	`static MLK_INLINE void mlk_keccak_f1600_x4_native(uint64_t *state)`
`17`	`17`	`{`
`18`		`- mlk_keccak_f1600_x4_scalar_v8a_asm_hybrid(state,`
	`18`	`+ mlk_keccak_f1600_x4_scalar_v8a_hybrid_asm(state,`
`19`	`19`	`mlk_keccakf1600_round_constants);`
`20`	`20`	`}`
`21`	`21`	`#endif /* !__ASSEMBLER__ */`