Skip to content

Commit 32b5350

Browse files
mkannwischermkannwischer
committed
FIPS202: Add dispatch for x4 xor_bytes and extract_bytes
Follow the same dispatch pattern used by mld_keccakf1600_permute and mld_keccakf1600x4_permute: extract the C fallback into a static _c function, have the public function dispatch via the native return code, and mark the native wrappers with MLD_MUST_CHECK_RETURN_VALUE. Add CBMC contracts for the native xor_bytes and extract_bytes functions and corresponding proofs for the native dispatch paths. The _c functions do not have separate proofs, in line with the other FIPS-202 functions. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
1 parent bb40f72 commit 32b5350

6 files changed

Lines changed: 156 additions & 10 deletions

File tree

‎mldsa/src/fips202/keccakf1600.c‎

Lines changed: 48 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -80,11 +80,12 @@ void mld_keccakf1600_xor_bytes(uint64_t *state, const unsigned char *data,
8080
#endif /* !MLD_SYS_LITTLE_ENDIAN */
8181
}
8282

83-
MLD_INTERNAL_API
84-
void mld_keccakf1600x4_extract_bytes(uint64_t *state, unsigned char *data0,
85-
unsigned char *data1, unsigned char *data2,
86-
unsigned char *data3, unsigned offset,
87-
unsigned length)
83+
static void mld_keccakf1600x4_extract_bytes_c(uint64_t *state,
84+
unsigned char *data0,
85+
unsigned char *data1,
86+
unsigned char *data2,
87+
unsigned char *data3,
88+
unsigned offset, unsigned length)
8889
{
8990
mld_keccakf1600_extract_bytes(state + MLD_KECCAK_LANES * 0, data0, offset,
9091
length);
@@ -97,11 +98,29 @@ void mld_keccakf1600x4_extract_bytes(uint64_t *state, unsigned char *data0,
9798
}
9899

99100
MLD_INTERNAL_API
100-
void mld_keccakf1600x4_xor_bytes(uint64_t *state, const unsigned char *data0,
101-
const unsigned char *data1,
102-
const unsigned char *data2,
103-
const unsigned char *data3, unsigned offset,
104-
unsigned length)
101+
void mld_keccakf1600x4_extract_bytes(uint64_t *state, unsigned char *data0,
102+
unsigned char *data1, unsigned char *data2,
103+
unsigned char *data3, unsigned offset,
104+
unsigned length)
105+
{
106+
#if defined(MLD_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE)
107+
if (mld_keccakf1600_extract_bytes_x4_native(state, data0, data1, data2, data3,
108+
offset, length) ==
109+
MLD_NATIVE_FUNC_SUCCESS)
110+
{
111+
return;
112+
}
113+
#endif /* MLD_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE */
114+
mld_keccakf1600x4_extract_bytes_c(state, data0, data1, data2, data3, offset,
115+
length);
116+
}
117+
118+
static void mld_keccakf1600x4_xor_bytes_c(uint64_t *state,
119+
const unsigned char *data0,
120+
const unsigned char *data1,
121+
const unsigned char *data2,
122+
const unsigned char *data3,
123+
unsigned offset, unsigned length)
105124
{
106125
mld_keccakf1600_xor_bytes(state + MLD_KECCAK_LANES * 0, data0, offset,
107126
length);
@@ -113,6 +132,25 @@ void mld_keccakf1600x4_xor_bytes(uint64_t *state, const unsigned char *data0,
113132
length);
114133
}
115134

135+
MLD_INTERNAL_API
136+
void mld_keccakf1600x4_xor_bytes(uint64_t *state, const unsigned char *data0,
137+
const unsigned char *data1,
138+
const unsigned char *data2,
139+
const unsigned char *data3, unsigned offset,
140+
unsigned length)
141+
{
142+
#if defined(MLD_USE_FIPS202_X4_XOR_BYTES_NATIVE)
143+
if (mld_keccakf1600_xor_bytes_x4_native(state, data0, data1, data2, data3,
144+
offset,
145+
length) == MLD_NATIVE_FUNC_SUCCESS)
146+
{
147+
return;
148+
}
149+
#endif /* MLD_USE_FIPS202_X4_XOR_BYTES_NATIVE */
150+
mld_keccakf1600x4_xor_bytes_c(state, data0, data1, data2, data3, offset,
151+
length);
152+
}
153+
116154
MLD_INTERNAL_API
117155
void mld_keccakf1600x4_permute(uint64_t *state)
118156
{

‎proofs/cbmc/dummy_backend_fips202_x4.h‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,8 @@
88

99

1010
#define MLD_USE_FIPS202_X4_NATIVE
11+
#define MLD_USE_FIPS202_X4_XOR_BYTES_NATIVE
12+
#define MLD_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE
1113

1214
#include "../../mldsa/src/fips202/native/api.h"
1315

‎proofs/cbmc/keccakf1600x4_extract_bytes_native/Makefile‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
# Copyright (c) The mldsa-native project authors
2+
# Copyright (c) The mlkem-native project authors
3+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
5+
include ../Makefile_params.common
6+
7+
HARNESS_ENTRY = harness
8+
HARNESS_FILE = keccakf1600x4_extract_bytes_native_harness
9+
10+
# This should be a unique identifier for this proof, and will appear on the
11+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
12+
PROOF_UID = keccakf1600x4_extract_bytes_native
13+
14+
DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 -DMLD_CONFIG_FIPS202_BACKEND_FILE="\"dummy_backend_fips202_x4.h\""
15+
INCLUDES +=
16+
17+
REMOVE_FUNCTION_BODY +=
18+
UNWINDSET +=
19+
20+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
21+
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/fips202/keccakf1600.c
22+
23+
CHECK_FUNCTION_CONTRACTS=mld_keccakf1600x4_extract_bytes
24+
USE_FUNCTION_CONTRACTS=mld_keccakf1600_extract_bytes_x4_native
25+
APPLY_LOOP_CONTRACTS=on
26+
USE_DYNAMIC_FRAMES=1
27+
28+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
29+
EXTERNAL_SAT_SOLVER=
30+
CBMCFLAGS=--bitwuzla
31+
32+
FUNCTION_NAME = keccakf1600x4_extract_bytes_native
33+
34+
# This function is large enough to need...
35+
CBMC_OBJECT_BITS = 8
36+
37+
include ../Makefile.common

‎proofs/cbmc/keccakf1600x4_extract_bytes_native/keccakf1600x4_extract_bytes_native_harness.c‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
// Copyright (c) The mlkem-native project authors
2+
// Copyright (c) The mldsa-native project authors
3+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
4+
// SPDX-License-Identifier: MIT-0
5+
6+
#include <keccakf1600.h>
7+
8+
void harness(void)
9+
{
10+
uint64_t *state;
11+
unsigned char *data0, *data1, *data2, *data3;
12+
unsigned offset;
13+
unsigned length;
14+
mld_keccakf1600x4_extract_bytes(state, data0, data1, data2, data3, offset,
15+
length);
16+
}

‎proofs/cbmc/keccakf1600x4_xor_bytes_native/Makefile‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
# Copyright (c) The mldsa-native project authors
2+
# Copyright (c) The mlkem-native project authors
3+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
4+
5+
include ../Makefile_params.common
6+
7+
HARNESS_ENTRY = harness
8+
HARNESS_FILE = keccakf1600x4_xor_bytes_native_harness
9+
10+
# This should be a unique identifier for this proof, and will appear on the
11+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
12+
PROOF_UID = keccakf1600x4_xor_bytes_native
13+
14+
DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 -DMLD_CONFIG_FIPS202_BACKEND_FILE="\"dummy_backend_fips202_x4.h\""
15+
INCLUDES +=
16+
17+
REMOVE_FUNCTION_BODY +=
18+
UNWINDSET +=
19+
20+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
21+
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/fips202/keccakf1600.c
22+
23+
CHECK_FUNCTION_CONTRACTS=mld_keccakf1600x4_xor_bytes
24+
USE_FUNCTION_CONTRACTS=mld_keccakf1600_xor_bytes_x4_native
25+
APPLY_LOOP_CONTRACTS=on
26+
USE_DYNAMIC_FRAMES=1
27+
28+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
29+
EXTERNAL_SAT_SOLVER=
30+
CBMCFLAGS=--bitwuzla
31+
32+
FUNCTION_NAME = keccakf1600x4_xor_bytes_native
33+
34+
# This function is large enough to need...
35+
CBMC_OBJECT_BITS = 8
36+
37+
include ../Makefile.common

‎proofs/cbmc/keccakf1600x4_xor_bytes_native/keccakf1600x4_xor_bytes_native_harness.c‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
// Copyright (c) The mlkem-native project authors
2+
// Copyright (c) The mldsa-native project authors
3+
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
4+
// SPDX-License-Identifier: MIT-0
5+
6+
#include <keccakf1600.h>
7+
8+
void harness(void)
9+
{
10+
uint64_t *state;
11+
const unsigned char *data0, *data1, *data2, *data3;
12+
unsigned offset;
13+
unsigned length;
14+
mld_keccakf1600x4_xor_bytes(state, data0, data1, data2, data3, offset,
15+
length);
16+
}

0 commit comments

Comments
 (0)