Skip to content

Commit df8d623

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

File tree

4 files changed

+116
-31
lines changed

4 files changed

+116
-31
lines changed

‎mldsa/src/poly_kl.c‎

Lines changed: 45 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,7 @@
3333
* within a single compilation unit. */
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)
36+
#define mld_poly_use_hint_c MLD_ADD_PARAM_SET(mld_poly_use_hint_c)
3637
/* End of parameter set namespacing */
3738

3839

@@ -123,40 +124,21 @@ unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0,
123124
return s;
124125
}
125126

126-
MLD_INTERNAL_API
127-
void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h)
127+
MLD_STATIC_TESTABLE void mld_poly_use_hint_c(mld_poly *b, const mld_poly *a,
128+
const mld_poly *h)
129+
__contract__(
130+
requires(memory_no_alias(a, sizeof(mld_poly)))
131+
requires(memory_no_alias(b, sizeof(mld_poly)))
132+
requires(memory_no_alias(h, sizeof(mld_poly)))
133+
requires(array_bound(a->coeffs, 0, MLDSA_N, 0, MLDSA_Q))
134+
requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2))
135+
assigns(memory_slice(b, sizeof(mld_poly)))
136+
ensures(array_bound(b->coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2)))
137+
)
128138
{
129139
unsigned int i;
130140
mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q);
131141
mld_assert_bound(h->coeffs, MLDSA_N, 0, 2);
132-
#if defined(MLD_USE_NATIVE_POLY_USE_HINT_88) && MLD_CONFIG_PARAMETER_SET == 44
133-
{
134-
int ret;
135-
/* TODO: proof */
136-
ret = mld_poly_use_hint_88_native(b->coeffs, a->coeffs, h->coeffs);
137-
if (ret == MLD_NATIVE_FUNC_SUCCESS)
138-
{
139-
mld_assert_bound(b->coeffs, MLDSA_N, 0,
140-
(MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
141-
return;
142-
}
143-
}
144-
#elif defined(MLD_USE_NATIVE_POLY_USE_HINT_32) && \
145-
(MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
146-
{
147-
int ret;
148-
/* TODO: proof */
149-
ret = mld_poly_use_hint_32_native(b->coeffs, a->coeffs, h->coeffs);
150-
if (ret == MLD_NATIVE_FUNC_SUCCESS)
151-
{
152-
mld_assert_bound(b->coeffs, MLDSA_N, 0,
153-
(MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
154-
return;
155-
}
156-
}
157-
#endif /* !(MLD_USE_NATIVE_POLY_USE_HINT_88 && MLD_CONFIG_PARAMETER_SET == 44) \
158-
&& MLD_USE_NATIVE_POLY_USE_HINT_32 && (MLD_CONFIG_PARAMETER_SET == \
159-
65 || MLD_CONFIG_PARAMETER_SET == 87) */
160142

161143
for (i = 0; i < MLDSA_N; ++i)
162144
__loop__(
@@ -169,6 +151,38 @@ void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h)
169151
mld_assert_bound(b->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
170152
}
171153

154+
MLD_INTERNAL_API
155+
void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h)
156+
{
157+
#if defined(MLD_USE_NATIVE_POLY_USE_HINT_88) && MLD_CONFIG_PARAMETER_SET == 44
158+
int ret;
159+
mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q);
160+
mld_assert_bound(h->coeffs, MLDSA_N, 0, 2);
161+
/* TODO: proof */
162+
ret = mld_poly_use_hint_88_native(b->coeffs, a->coeffs, h->coeffs);
163+
if (ret == MLD_NATIVE_FUNC_SUCCESS)
164+
{
165+
mld_assert_bound(b->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
166+
return;
167+
}
168+
#elif defined(MLD_USE_NATIVE_POLY_USE_HINT_32) && \
169+
(MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87)
170+
int ret;
171+
mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q);
172+
mld_assert_bound(h->coeffs, MLDSA_N, 0, 2);
173+
/* TODO: proof */
174+
ret = mld_poly_use_hint_32_native(b->coeffs, a->coeffs, h->coeffs);
175+
if (ret == MLD_NATIVE_FUNC_SUCCESS)
176+
{
177+
mld_assert_bound(b->coeffs, MLDSA_N, 0, (MLDSA_Q - 1) / (2 * MLDSA_GAMMA2));
178+
return;
179+
}
180+
#endif /* !(MLD_USE_NATIVE_POLY_USE_HINT_88 && MLD_CONFIG_PARAMETER_SET == 44) \
181+
&& MLD_USE_NATIVE_POLY_USE_HINT_32 && (MLD_CONFIG_PARAMETER_SET == \
182+
65 || MLD_CONFIG_PARAMETER_SET == 87) */
183+
mld_poly_use_hint_c(b, a, h);
184+
}
185+
172186
/*************************************************
173187
* Name: mld_rej_eta
174188
*
@@ -880,6 +894,7 @@ void mld_polyw1_pack(uint8_t r[MLDSA_POLYW1_PACKEDBYTES], const mld_poly *a)
880894
* Don't modify by hand -- this is auto-generated by scripts/autogen. */
881895
#undef mld_rej_eta
882896
#undef mld_poly_decompose_c
897+
#undef mld_poly_use_hint_c
883898
#undef POLY_UNIFORM_ETA_NBLOCKS
884899
#undef POLY_UNIFORM_ETA_NBLOCKS
885900
#undef POLY_UNIFORM_GAMMA1_NBLOCKS

‎proofs/cbmc/poly_use_hint/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)poly_use_hint
23-
USE_FUNCTION_CONTRACTS=mld_use_hint
23+
USE_FUNCTION_CONTRACTS=mld_poly_use_hint_c
2424
APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1
2626

‎proofs/cbmc/poly_use_hint_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 = poly_use_hint_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 = poly_use_hint_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_poly_use_hint_c
23+
USE_FUNCTION_CONTRACTS=mld_use_hint
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_poly_use_hint_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/poly_use_hint_c/poly_use_hint_c_harness.c‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
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+
// Prototype for the function under test
7+
#define mld_poly_use_hint_c MLD_ADD_PARAM_SET(mld_poly_use_hint_c)
8+
void mld_poly_use_hint_c(mld_poly *b, mld_poly *a, mld_poly *h);
9+
10+
11+
void harness(void)
12+
{
13+
mld_poly *a, *b, *h;
14+
mld_poly_use_hint_c(b, a, h);
15+
}

0 commit comments

Comments
 (0)