Skip to content

Commit 97c3b6a

Browse files
willieyzwillieyz
committed
Hoist default C backend into separate functions(mld_polyz_unpack_c)
Signed-off-by: willieyz <willie.zhao@chelpis.com>
1 parent df8d623 commit 97c3b6a

File tree

4 files changed

+112
-26
lines changed

4 files changed

+112
-26
lines changed

‎mldsa/src/poly_kl.c‎

Lines changed: 39 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@
3434
#define mld_rej_eta MLD_ADD_PARAM_SET(mld_rej_eta)
3535
#define mld_poly_decompose_c MLD_ADD_PARAM_SET(mld_poly_decompose_c)
3636
#define mld_poly_use_hint_c MLD_ADD_PARAM_SET(mld_poly_use_hint_c)
37+
#define mld_polyz_unpack_c MLD_ADD_PARAM_SET(mld_polyz_unpack_c)
3738
/* End of parameter set namespacing */
3839

3940

@@ -776,33 +777,16 @@ void mld_polyz_pack(uint8_t r[MLDSA_POLYZ_PACKEDBYTES], const mld_poly *a)
776777
#endif /* MLD_CONFIG_PARAMETER_SET != 44 */
777778
}
778779

779-
MLD_INTERNAL_API
780-
void mld_polyz_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES])
780+
MLD_STATIC_TESTABLE void mld_polyz_unpack_c(
781+
mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES])
782+
__contract__(
783+
requires(memory_no_alias(r, sizeof(mld_poly)))
784+
requires(memory_no_alias(a, MLDSA_POLYZ_PACKEDBYTES))
785+
assigns(memory_slice(r, sizeof(mld_poly)))
786+
ensures(array_bound(r->coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1))
787+
)
781788
{
782789
unsigned int i;
783-
#if defined(MLD_USE_NATIVE_POLYZ_UNPACK_17) && MLD_CONFIG_PARAMETER_SET == 44
784-
/* TODO: proof */
785-
int ret;
786-
ret = mld_polyz_unpack_17_native(r->coeffs, a);
787-
if (ret == MLD_NATIVE_FUNC_SUCCESS)
788-
{
789-
mld_assert_bound(r->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1);
790-
return;
791-
}
792-
#elif defined(MLD_USE_NATIVE_POLYZ_UNPACK_19) && \
793-
(MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
794-
/* TODO: proof */
795-
int ret;
796-
ret = mld_polyz_unpack_19_native(r->coeffs, a);
797-
if (ret == MLD_NATIVE_FUNC_SUCCESS)
798-
{
799-
mld_assert_bound(r->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1);
800-
return;
801-
}
802-
#endif /* !(MLD_USE_NATIVE_POLYZ_UNPACK_17 && MLD_CONFIG_PARAMETER_SET == 44) \
803-
&& MLD_USE_NATIVE_POLYZ_UNPACK_19 && (MLD_CONFIG_PARAMETER_SET == 65 \
804-
|| MLD_CONFIG_PARAMETER_SET == 87) */
805-
806790
#if MLD_CONFIG_PARAMETER_SET == 44
807791
for (i = 0; i < MLDSA_N / 4; ++i)
808792
__loop__(
@@ -858,6 +842,35 @@ void mld_polyz_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES])
858842
mld_assert_bound(r->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1);
859843
}
860844

845+
MLD_INTERNAL_API
846+
void mld_polyz_unpack(mld_poly *r, const uint8_t a[MLDSA_POLYZ_PACKEDBYTES])
847+
{
848+
#if defined(MLD_USE_NATIVE_POLYZ_UNPACK_17) && MLD_CONFIG_PARAMETER_SET == 44
849+
/* TODO: proof */
850+
int ret;
851+
ret = mld_polyz_unpack_17_native(r->coeffs, a);
852+
if (ret == MLD_NATIVE_FUNC_SUCCESS)
853+
{
854+
mld_assert_bound(r->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1);
855+
return;
856+
}
857+
#elif defined(MLD_USE_NATIVE_POLYZ_UNPACK_19) && \
858+
(MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
859+
/* TODO: proof */
860+
int ret;
861+
ret = mld_polyz_unpack_19_native(r->coeffs, a);
862+
if (ret == MLD_NATIVE_FUNC_SUCCESS)
863+
{
864+
mld_assert_bound(r->coeffs, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1);
865+
return;
866+
}
867+
#endif /* !(MLD_USE_NATIVE_POLYZ_UNPACK_17 && MLD_CONFIG_PARAMETER_SET == 44) \
868+
&& MLD_USE_NATIVE_POLYZ_UNPACK_19 && (MLD_CONFIG_PARAMETER_SET == 65 \
869+
|| MLD_CONFIG_PARAMETER_SET == 87) */
870+
871+
mld_polyz_unpack_c(r, a);
872+
}
873+
861874
MLD_INTERNAL_API
862875
void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a)
863876
{
@@ -895,6 +908,7 @@ void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a)
895908
#undef mld_rej_eta
896909
#undef mld_poly_decompose_c
897910
#undef mld_poly_use_hint_c
911+
#undef mld_polyz_unpack_c
898912
#undef POLY_UNIFORM_ETA_NBLOCKS
899913
#undef POLY_UNIFORM_ETA_NBLOCKS
900914
#undef POLY_UNIFORM_GAMMA1_NBLOCKS

‎proofs/cbmc/polyz_unpack/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
2020
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c
2121

2222
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyz_unpack
23-
USE_FUNCTION_CONTRACTS=
23+
USE_FUNCTION_CONTRACTS=mld_polyz_unpack_c
2424
APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1
2626

‎proofs/cbmc/polyz_unpack_c/Makefile‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
# Copyright (c) The mldsa-native project authors
2+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
include ../Makefile_params.common
5+
6+
HARNESS_ENTRY = harness
7+
HARNESS_FILE = polyz_unpack_c_harness
8+
9+
# This should be a unique identifier for this proof, and will appear on the
10+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
11+
PROOF_UID = polyz_unpack_c
12+
13+
DEFINES +=
14+
INCLUDES +=
15+
16+
REMOVE_FUNCTION_BODY +=
17+
UNWINDSET +=
18+
19+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
20+
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c
21+
22+
CHECK_FUNCTION_CONTRACTS= mld_polyz_unpack_c
23+
USE_FUNCTION_CONTRACTS=
24+
APPLY_LOOP_CONTRACTS=on
25+
USE_DYNAMIC_FRAMES=1
26+
27+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
28+
EXTERNAL_SAT_SOLVER=
29+
CBMCFLAGS=--smt2
30+
31+
FUNCTION_NAME = mld_polyz_unpack_c
32+
33+
# If this proof is found to consume huge amounts of RAM, you can set the
34+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
35+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
36+
# documentation in Makefile.common under the "Job Pools" heading for details.
37+
# EXPENSIVE = true
38+
39+
# This function is large enough to need...
40+
CBMC_OBJECT_BITS = 8
41+
42+
# If you require access to a file-local ("static") function or object to conduct
43+
# your proof, set the following (and do not include the original source file
44+
# ("mldsa/poly.c") in PROJECT_SOURCES).
45+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
46+
# include ../Makefile.common
47+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c
48+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
49+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
50+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
51+
# be set before including Makefile.common, but any use of variables on the
52+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
53+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
54+
55+
include ../Makefile.common

‎proofs/cbmc/polyz_unpack_c/polyz_unpack_c_harness.c‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
// Copyright (c) The mldsa-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
#include "poly_kl.h"
5+
6+
7+
// Prototype for the function under test
8+
#define mld_polyz_unpack_c MLD_ADD_PARAM_SET(mld_polyz_unpack_c)
9+
void mld_polyz_unpack_c(mld_poly *a, uint8_t *b);
10+
11+
12+
void harness(void)
13+
{
14+
mld_poly *a;
15+
uint8_t *b;
16+
mld_polyz_unpack_c(a, b);
17+
}

0 commit comments

Comments
 (0)