Skip to content

FIPS202: Consolidate backend MLK_USE_NATIVE_* flags #1775

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mkannwischer wants to merge 1 commit into
base: main
Choose a base branch
from
Open

FIPS202: Consolidate backend MLK_USE_NATIVE_* flags #1775

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion dev/fips202/aarch64/x1_scalar.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
#define MLK_DEV_FIPS202_AARCH64_X1_SCALAR_H

/* Part of backend API */
#define MLK_USE_FIPS202_X1_NATIVE
#define MLK_USE_NATIVE_FIPS202_X1
/* Guard for assembly file */
#define MLK_FIPS202_AARCH64_NEED_X1_SCALAR

Expand Down
2 changes: 1 addition & 1 deletion dev/fips202/aarch64/x1_v84a.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
#endif

/* Part of backend API */
#define MLK_USE_FIPS202_X1_NATIVE
#define MLK_USE_NATIVE_FIPS202_X1
/* Guard for assembly file */
#define MLK_FIPS202_AARCH64_NEED_X1_V84A

Expand Down
2 changes: 1 addition & 1 deletion dev/fips202/aarch64/x2_v84a.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
#endif

/* Part of backend API */
#define MLK_USE_FIPS202_X4_NATIVE
#define MLK_USE_NATIVE_FIPS202_X4
/* Guard for assembly file */
#define MLK_FIPS202_AARCH64_NEED_X2_V84A

Expand Down
2 changes: 1 addition & 1 deletion dev/fips202/aarch64/x4_v8a_scalar.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
#define MLK_DEV_FIPS202_AARCH64_X4_V8A_SCALAR_H

/* Part of backend API */
#define MLK_USE_FIPS202_X4_NATIVE
#define MLK_USE_NATIVE_FIPS202_X4
/* Guard for assembly file */
#define MLK_FIPS202_AARCH64_NEED_X4_V8A_SCALAR_HYBRID

Expand Down
2 changes: 1 addition & 1 deletion dev/fips202/aarch64/x4_v8a_v84a_scalar.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
#endif

/* Part of backend API */
#define MLK_USE_FIPS202_X4_NATIVE
#define MLK_USE_NATIVE_FIPS202_X4
/* Guard for assembly file */
#define MLK_FIPS202_AARCH64_NEED_X4_V8A_V84A_SCALAR_HYBRID

Expand Down
6 changes: 3 additions & 3 deletions dev/fips202/armv81m/mve.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,9 @@
#define MLK_FIPS202_NATIVE_ARMV81M

/* Part of backend API */
#define MLK_USE_FIPS202_X4_NATIVE
#define MLK_USE_FIPS202_X4_XOR_BYTES_NATIVE
#define MLK_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE
#define MLK_USE_NATIVE_FIPS202_X4
#define MLK_USE_NATIVE_FIPS202_X4_XOR_BYTES
#define MLK_USE_NATIVE_FIPS202_X4_EXTRACT_BYTES
/* Guard for assembly file */
#define MLK_FIPS202_ARMV81M_NEED_X4

Expand Down
2 changes: 1 addition & 1 deletion dev/fips202/x86_64/keccak_f1600_x4_avx2.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
#define MLK_FIPS202_X86_64_NEED_X4_AVX2

/* Part of backend API */
#define MLK_USE_FIPS202_X4_NATIVE
#define MLK_USE_NATIVE_FIPS202_X4

#if !defined(__ASSEMBLER__)
#include "../api.h"
Expand Down
4 changes: 2 additions & 2 deletions examples/custom_backend/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ The configuration file [mlkem_native_config.h](mlkem_native/mlkem_native_config.

A custom backend consists of:
1. A metadata header (e.g., [custom.h](mlkem_native/src/fips202/native/custom/custom.h)) that:
- Sets `MLK_USE_FIPS202_X1_NATIVE` (and/or `X4`) to indicate which functions are replaced
- Sets `MLK_USE_NATIVE_FIPS202_X1` (and/or `X4`) to indicate which functions are replaced
- Includes the implementation header
2. An implementation providing `mlk_keccakf1600_native()` (and/or batched variants)

Expand All @@ -41,7 +41,7 @@ Example backend metadata file:
#define CUSTOM_FIPS202_BACKEND_H

/* Indicate we're replacing 1-fold Keccak-f1600 */
#define MLK_USE_FIPS202_X1_NATIVE
#define MLK_USE_NATIVE_FIPS202_X1

/* Include the implementation */
#include "custom/src/keccak_impl.h"
Expand Down
2 changes: 1 addition & 1 deletion examples/custom_backend/mlkem_native/src/fips202/native/custom/custom.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
#include "../api.h"
#include "src/sha3.h"
/* Replace (single) Keccak-F1600 by tiny-SHA3's */
#define MLK_USE_FIPS202_X1_NATIVE
#define MLK_USE_NATIVE_FIPS202_X1
static MLK_INLINE int mlk_keccak_f1600_x1_native(uint64_t *state)
{
tiny_sha3_keccakf(state);
Expand Down
18 changes: 9 additions & 9 deletions mlkem/mlkem_native.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -463,23 +463,23 @@
/* mlkem/src/fips202/native/aarch64/x1_scalar.h */
#undef MLK_FIPS202_AARCH64_NEED_X1_SCALAR
#undef MLK_FIPS202_NATIVE_AARCH64_X1_SCALAR_H
#undef MLK_USE_FIPS202_X1_NATIVE
#undef MLK_USE_NATIVE_FIPS202_X1
/* mlkem/src/fips202/native/aarch64/x1_v84a.h */
#undef MLK_FIPS202_AARCH64_NEED_X1_V84A
#undef MLK_FIPS202_NATIVE_AARCH64_X1_V84A_H
#undef MLK_USE_FIPS202_X1_NATIVE
#undef MLK_USE_NATIVE_FIPS202_X1
/* mlkem/src/fips202/native/aarch64/x2_v84a.h */
#undef MLK_FIPS202_AARCH64_NEED_X2_V84A
#undef MLK_FIPS202_NATIVE_AARCH64_X2_V84A_H
#undef MLK_USE_FIPS202_X4_NATIVE
#undef MLK_USE_NATIVE_FIPS202_X4
/* mlkem/src/fips202/native/aarch64/x4_v8a_scalar.h */
#undef MLK_FIPS202_AARCH64_NEED_X4_V8A_SCALAR_HYBRID
#undef MLK_FIPS202_NATIVE_AARCH64_X4_V8A_SCALAR_H
#undef MLK_USE_FIPS202_X4_NATIVE
#undef MLK_USE_NATIVE_FIPS202_X4
/* mlkem/src/fips202/native/aarch64/x4_v8a_v84a_scalar.h */
#undef MLK_FIPS202_AARCH64_NEED_X4_V8A_V84A_SCALAR_HYBRID
#undef MLK_FIPS202_NATIVE_AARCH64_X4_V8A_V84A_SCALAR_H
#undef MLK_USE_FIPS202_X4_NATIVE
#undef MLK_USE_NATIVE_FIPS202_X4
#endif /* MLK_SYS_AARCH64 */
#if defined(MLK_SYS_X86_64)
/*
Expand All @@ -488,7 +488,7 @@
/* mlkem/src/fips202/native/x86_64/keccak_f1600_x4_avx2.h */
#undef MLK_FIPS202_NATIVE_X86_64_KECCAK_F1600_X4_AVX2_H
#undef MLK_FIPS202_X86_64_NEED_X4_AVX2
#undef MLK_USE_FIPS202_X4_NATIVE
#undef MLK_USE_NATIVE_FIPS202_X4
/* mlkem/src/fips202/native/x86_64/src/fips202_native_x86_64.h */
#undef MLK_FIPS202_NATIVE_X86_64_SRC_FIPS202_NATIVE_X86_64_H
#undef mlk_keccak_f1600_x4_avx2_asm
Expand All @@ -504,9 +504,9 @@
#undef MLK_FIPS202_ARMV81M_NEED_X4
#undef MLK_FIPS202_NATIVE_ARMV81M
#undef MLK_FIPS202_NATIVE_ARMV81M_MVE_H
#undef MLK_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE
#undef MLK_USE_FIPS202_X4_NATIVE
#undef MLK_USE_FIPS202_X4_XOR_BYTES_NATIVE
#undef MLK_USE_NATIVE_FIPS202_X4
#undef MLK_USE_NATIVE_FIPS202_X4_EXTRACT_BYTES
#undef MLK_USE_NATIVE_FIPS202_X4_XOR_BYTES
#undef mlk_keccak_f1600_x4_native_impl
#undef mlk_keccak_f1600_x4_state_extract_bytes
#undef mlk_keccak_f1600_x4_state_xor_bytes
Expand Down
18 changes: 9 additions & 9 deletions mlkem/mlkem_native_asm.S
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -487,23 +487,23 @@
/* mlkem/src/fips202/native/aarch64/x1_scalar.h */
#undef MLK_FIPS202_AARCH64_NEED_X1_SCALAR
#undef MLK_FIPS202_NATIVE_AARCH64_X1_SCALAR_H
#undef MLK_USE_FIPS202_X1_NATIVE
#undef MLK_USE_NATIVE_FIPS202_X1
/* mlkem/src/fips202/native/aarch64/x1_v84a.h */
#undef MLK_FIPS202_AARCH64_NEED_X1_V84A
#undef MLK_FIPS202_NATIVE_AARCH64_X1_V84A_H
#undef MLK_USE_FIPS202_X1_NATIVE
#undef MLK_USE_NATIVE_FIPS202_X1
/* mlkem/src/fips202/native/aarch64/x2_v84a.h */
#undef MLK_FIPS202_AARCH64_NEED_X2_V84A
#undef MLK_FIPS202_NATIVE_AARCH64_X2_V84A_H
#undef MLK_USE_FIPS202_X4_NATIVE
#undef MLK_USE_NATIVE_FIPS202_X4
/* mlkem/src/fips202/native/aarch64/x4_v8a_scalar.h */
#undef MLK_FIPS202_AARCH64_NEED_X4_V8A_SCALAR_HYBRID
#undef MLK_FIPS202_NATIVE_AARCH64_X4_V8A_SCALAR_H
#undef MLK_USE_FIPS202_X4_NATIVE
#undef MLK_USE_NATIVE_FIPS202_X4
/* mlkem/src/fips202/native/aarch64/x4_v8a_v84a_scalar.h */
#undef MLK_FIPS202_AARCH64_NEED_X4_V8A_V84A_SCALAR_HYBRID
#undef MLK_FIPS202_NATIVE_AARCH64_X4_V8A_V84A_SCALAR_H
#undef MLK_USE_FIPS202_X4_NATIVE
#undef MLK_USE_NATIVE_FIPS202_X4
#endif /* MLK_SYS_AARCH64 */
#if defined(MLK_SYS_X86_64)
/*
Expand All @@ -512,7 +512,7 @@
/* mlkem/src/fips202/native/x86_64/keccak_f1600_x4_avx2.h */
#undef MLK_FIPS202_NATIVE_X86_64_KECCAK_F1600_X4_AVX2_H
#undef MLK_FIPS202_X86_64_NEED_X4_AVX2
#undef MLK_USE_FIPS202_X4_NATIVE
#undef MLK_USE_NATIVE_FIPS202_X4
/* mlkem/src/fips202/native/x86_64/src/fips202_native_x86_64.h */
#undef MLK_FIPS202_NATIVE_X86_64_SRC_FIPS202_NATIVE_X86_64_H
#undef mlk_keccak_f1600_x4_avx2_asm
Expand All @@ -528,9 +528,9 @@
#undef MLK_FIPS202_ARMV81M_NEED_X4
#undef MLK_FIPS202_NATIVE_ARMV81M
#undef MLK_FIPS202_NATIVE_ARMV81M_MVE_H
#undef MLK_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE
#undef MLK_USE_FIPS202_X4_NATIVE
#undef MLK_USE_FIPS202_X4_XOR_BYTES_NATIVE
#undef MLK_USE_NATIVE_FIPS202_X4
#undef MLK_USE_NATIVE_FIPS202_X4_EXTRACT_BYTES
#undef MLK_USE_NATIVE_FIPS202_X4_XOR_BYTES
#undef mlk_keccak_f1600_x4_native_impl
#undef mlk_keccak_f1600_x4_state_extract_bytes
#undef mlk_keccak_f1600_x4_state_xor_bytes
Expand Down
4 changes: 2 additions & 2 deletions mlkem/src/fips202/fips202.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -132,12 +132,12 @@ __contract__(
);

#if !defined(MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202) || \
!defined(MLK_USE_FIPS202_X4_NATIVE)
!defined(MLK_USE_NATIVE_FIPS202_X4)
/* If you provide your own FIPS-202 implementation where the x4-
* Keccak-f1600-x4 implementation falls back to 4-fold Keccak-f1600,
* set this to gain a small speedup. */
#define FIPS202_X4_DEFAULT_IMPLEMENTATION
#endif /* !MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 || !MLK_USE_FIPS202_X4_NATIVE \
#endif /* !MLK_CONFIG_USE_NATIVE_BACKEND_FIPS202 || !MLK_USE_NATIVE_FIPS202_X4 \
*/


Expand Down
16 changes: 8 additions & 8 deletions mlkem/src/fips202/keccakf1600.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,14 +115,14 @@ void mlk_keccakf1600x4_extract_bytes(uint64_t *state, unsigned char *data0,
unsigned char *data3, unsigned offset,
unsigned length)
{
#if defined(MLK_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE)
#if defined(MLK_USE_NATIVE_FIPS202_X4_EXTRACT_BYTES)
if (mlk_keccakf1600_extract_bytes_x4_native(state, data0, data1, data2, data3,
offset, length) ==
MLK_NATIVE_FUNC_SUCCESS)
{
return;
}
#endif /* MLK_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE */
#endif /* MLK_USE_NATIVE_FIPS202_X4_EXTRACT_BYTES */
mlk_keccakf1600x4_extract_bytes_c(state, data0, data1, data2, data3, offset,
length);
}
Expand Down Expand Up @@ -164,26 +164,26 @@ void mlk_keccakf1600x4_xor_bytes(uint64_t *state, const unsigned char *data0,
const unsigned char *data3, unsigned offset,
unsigned length)
{
#if defined(MLK_USE_FIPS202_X4_XOR_BYTES_NATIVE)
#if defined(MLK_USE_NATIVE_FIPS202_X4_XOR_BYTES)
if (mlk_keccakf1600_xor_bytes_x4_native(state, data0, data1, data2, data3,
offset,
length) == MLK_NATIVE_FUNC_SUCCESS)
{
return;
}
#endif /* MLK_USE_FIPS202_X4_XOR_BYTES_NATIVE */
#endif /* MLK_USE_NATIVE_FIPS202_X4_XOR_BYTES */
mlk_keccakf1600x4_xor_bytes_c(state, data0, data1, data2, data3, offset,
length);
}

void mlk_keccakf1600x4_permute(uint64_t *state)
{
#if defined(MLK_USE_FIPS202_X4_NATIVE)
#if defined(MLK_USE_NATIVE_FIPS202_X4)
if (mlk_keccak_f1600_x4_native(state) == MLK_NATIVE_FUNC_SUCCESS)
{
return;
}
#endif /* MLK_USE_FIPS202_X4_NATIVE */
#endif /* MLK_USE_NATIVE_FIPS202_X4 */
mlk_keccakf1600_permute(state + MLK_KECCAK_LANES * 0);
mlk_keccakf1600_permute(state + MLK_KECCAK_LANES * 1);
mlk_keccakf1600_permute(state + MLK_KECCAK_LANES * 2);
Expand Down Expand Up @@ -478,12 +478,12 @@ __contract__(

void mlk_keccakf1600_permute(uint64_t *state)
{
#if defined(MLK_USE_FIPS202_X1_NATIVE)
#if defined(MLK_USE_NATIVE_FIPS202_X1)
if (mlk_keccak_f1600_x1_native(state) == MLK_NATIVE_FUNC_SUCCESS)
{
return;
}
#endif /* MLK_USE_FIPS202_X1_NATIVE */
#endif /* MLK_USE_NATIVE_FIPS202_X1 */
mlk_keccakf1600_permute_c(state);
}

Expand Down
2 changes: 1 addition & 1 deletion mlkem/src/fips202/native/aarch64/x1_scalar.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
#define MLK_FIPS202_NATIVE_AARCH64_X1_SCALAR_H

/* Part of backend API */
#define MLK_USE_FIPS202_X1_NATIVE
#define MLK_USE_NATIVE_FIPS202_X1
/* Guard for assembly file */
#define MLK_FIPS202_AARCH64_NEED_X1_SCALAR

Expand Down
2 changes: 1 addition & 1 deletion mlkem/src/fips202/native/aarch64/x1_v84a.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
#endif

/* Part of backend API */
#define MLK_USE_FIPS202_X1_NATIVE
#define MLK_USE_NATIVE_FIPS202_X1
/* Guard for assembly file */
#define MLK_FIPS202_AARCH64_NEED_X1_V84A

Expand Down
2 changes: 1 addition & 1 deletion mlkem/src/fips202/native/aarch64/x2_v84a.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
#endif

/* Part of backend API */
#define MLK_USE_FIPS202_X4_NATIVE
#define MLK_USE_NATIVE_FIPS202_X4
/* Guard for assembly file */
#define MLK_FIPS202_AARCH64_NEED_X2_V84A

Expand Down
2 changes: 1 addition & 1 deletion mlkem/src/fips202/native/aarch64/x4_v8a_scalar.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
#define MLK_FIPS202_NATIVE_AARCH64_X4_V8A_SCALAR_H

/* Part of backend API */
#define MLK_USE_FIPS202_X4_NATIVE
#define MLK_USE_NATIVE_FIPS202_X4
/* Guard for assembly file */
#define MLK_FIPS202_AARCH64_NEED_X4_V8A_SCALAR_HYBRID

Expand Down
2 changes: 1 addition & 1 deletion mlkem/src/fips202/native/aarch64/x4_v8a_v84a_scalar.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
#endif

/* Part of backend API */
#define MLK_USE_FIPS202_X4_NATIVE
#define MLK_USE_NATIVE_FIPS202_X4
/* Guard for assembly file */
#define MLK_FIPS202_AARCH64_NEED_X4_V8A_V84A_SCALAR_HYBRID

Expand Down
22 changes: 11 additions & 11 deletions mlkem/src/fips202/native/api.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,30 +29,30 @@
* A _backend_ is a specific implementation of parts of this interface.
*
* You can replace 1-fold or 4-fold batched Keccak-F1600.
* To enable, set MLK_USE_FIPS202_X1_NATIVE or MLK_USE_FIPS202_X4_NATIVE
* To enable, set MLK_USE_NATIVE_FIPS202_X1 or MLK_USE_NATIVE_FIPS202_X4
* in your backend, and define the inline wrappers mlk_keccak_f1600_x1_native()
* and/or mlk_keccak_f1600_x4_native(), respectively, to forward to your
* implementation.
*/

#if defined(MLK_USE_FIPS202_X1_NATIVE)
#if defined(MLK_USE_NATIVE_FIPS202_X1)
MLK_MUST_CHECK_RETURN_VALUE
static MLK_INLINE int mlk_keccak_f1600_x1_native(uint64_t *state)
__contract__(
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1))
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1))
ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS)
ensures((return_value == MLK_NATIVE_FUNC_FALLBACK) ==> array_unchanged_u64(state, 25 * 1)));
#endif /* MLK_USE_FIPS202_X1_NATIVE */
#if defined(MLK_USE_FIPS202_X4_NATIVE)
#endif /* MLK_USE_NATIVE_FIPS202_X1 */
#if defined(MLK_USE_NATIVE_FIPS202_X4)
MLK_MUST_CHECK_RETURN_VALUE
static MLK_INLINE int mlk_keccak_f1600_x4_native(uint64_t *state)
__contract__(
requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4))
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4))
ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS)
ensures((return_value == MLK_NATIVE_FUNC_FALLBACK) ==> array_unchanged_u64(state, 25 * 4)));
#endif /* MLK_USE_FIPS202_X4_NATIVE */
#endif /* MLK_USE_NATIVE_FIPS202_X4 */

/*
* Native x4 XOR bytes and extract bytes interface.
Expand All @@ -66,12 +66,12 @@ __contract__(
* NOTE: We assume that the custom representation of the zero state is the
* all-zero state.
*
* MLK_USE_FIPS202_X4_XOR_BYTES_NATIVE: Backend provides native XOR bytes
* MLK_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE: Backend provides native extract
* MLK_USE_NATIVE_FIPS202_X4_XOR_BYTES: Backend provides native XOR bytes
* MLK_USE_NATIVE_FIPS202_X4_EXTRACT_BYTES: Backend provides native extract
* bytes
*/

#if defined(MLK_USE_FIPS202_X4_XOR_BYTES_NATIVE)
#if defined(MLK_USE_NATIVE_FIPS202_X4_XOR_BYTES)
MLK_MUST_CHECK_RETURN_VALUE
static MLK_INLINE int mlk_keccakf1600_xor_bytes_x4_native(
uint64_t *state, const unsigned char *data0, const unsigned char *data1,
Expand All @@ -91,9 +91,9 @@ __contract__(
assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4))
ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS)
ensures((return_value == MLK_NATIVE_FUNC_FALLBACK) ==> array_unchanged_u64(state, 25 * 4)));
#endif /* MLK_USE_FIPS202_X4_XOR_BYTES_NATIVE */
#endif /* MLK_USE_NATIVE_FIPS202_X4_XOR_BYTES */

#if defined(MLK_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE)
#if defined(MLK_USE_NATIVE_FIPS202_X4_EXTRACT_BYTES)
MLK_MUST_CHECK_RETURN_VALUE
static MLK_INLINE int mlk_keccakf1600_extract_bytes_x4_native(
uint64_t *state, unsigned char *data0, unsigned char *data1,
Expand All @@ -112,6 +112,6 @@ __contract__(
assigns(memory_slice(data2, length))
assigns(memory_slice(data3, length))
ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS));
#endif /* MLK_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE */
#endif /* MLK_USE_NATIVE_FIPS202_X4_EXTRACT_BYTES */

#endif /* !MLK_FIPS202_NATIVE_API_H */
Loading
Loading