Skip to content

Commit 6fef01b

Browse files
willieyzwillieyz
committed
CBMC: apply same workarounds for mld_polymat_permute_bitrev_to_custom
- This commit apply same workarounds for mld_polymat_permute_bitrev_to_custom, reference from mlkem-native, add following function and corresponding CBMC proof: - mld_polyvecl_permute_bitrev_to_custom - mld_polyvecl_permute_bitrev_to_custom_native - and for the CBMC proof for above function: - mld_polyvecl_permute_bitrev_to_custom_native we add the contract and exception in check-contracts for for mld_poly_permute_bitrev_to_custom. - Use tests cbmc -p polymat_permute_bitrev_to_custom contract in polymat_permute_bitrev_to_custom cbmc proof Signed-off-by: willieyz <[email protected]> add changes Signed-off-by: willieyz <[email protected]>
1 parent 34281c3 commit 6fef01b

File tree

9 files changed

+189
-16
lines changed

9 files changed

+189
-16
lines changed

‎mldsa/src/native/api.h‎

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -122,7 +122,16 @@ set if there are native implementations for NTT and INTT."
122122
* Arguments: - int32_t p[MLDSA_N]: pointer to in/output polynomial
123123
*
124124
**************************************************/
125-
static MLD_INLINE void mld_poly_permute_bitrev_to_custom(int32_t p[MLDSA_N]);
125+
static MLD_INLINE void mld_poly_permute_bitrev_to_custom(int32_t p[MLDSA_N])
126+
__contract__(
127+
/* We don't specify that this should be a permutation, but only
128+
* that it does not change the bound established at the end of
129+
* mld_polyvec_matrix_expand.
130+
*/
131+
requires(memory_no_alias(p, sizeof(int32_t) * MLDSA_N))
132+
requires(array_bound(p, 0, MLDSA_N, 0, MLDSA_Q))
133+
assigns(memory_slice(p, sizeof(int32_t) * MLDSA_N))
134+
ensures(array_bound(p, 0, MLDSA_N, 0, MLDSA_Q)));
126135
#endif /* MLD_USE_NATIVE_NTT_CUSTOM_ORDER */
127136

128137

‎mldsa/src/polyvec.c‎

Lines changed: 41 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,8 @@
2525
* with native backends, which are currently not yet namespaced. */
2626
#define mld_polymat_permute_bitrev_to_custom \
2727
MLD_ADD_PARAM_SET(mld_polymat_permute_bitrev_to_custom)
28+
#define mld_polyvecl_permute_bitrev_to_custom \
29+
MLD_ADD_PARAM_SET(mld_polyvecl_permute_bitrev_to_custom)
2830
#define mld_polyvecl_pointwise_acc_montgomery_c \
2931
MLD_ADD_PARAM_SET(mld_polyvecl_pointwise_acc_montgomery_c)
3032

@@ -33,6 +35,37 @@
3335
* of coefficients.
3436
* No-op unless a native backend with a custom ordering is used.
3537
*/
38+
39+
static void mld_polyvecl_permute_bitrev_to_custom(mld_polyvecl *v)
40+
__contract__(
41+
/* We don't specify that this should be a permutation, but only
42+
* that it does not change the bound established at the end of
43+
* mld_polyvec_matrix_expand.
44+
*/
45+
requires(memory_no_alias(v, sizeof(mld_polyvecl)))
46+
requires(forall(x, 0, MLDSA_L,
47+
array_bound(v->vec[x].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))
48+
assigns(memory_slice(v, sizeof(mld_polyvecl)))
49+
ensures(forall(x, 0, MLDSA_L,
50+
array_bound(v->vec[x].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
51+
{
52+
#if defined(MLD_USE_NATIVE_NTT_CUSTOM_ORDER)
53+
unsigned i;
54+
for (i = 0; i < MLDSA_L; i++)
55+
__loop__(
56+
assigns(i, memory_slice(v, sizeof(mld_polyvecl)))
57+
invariant(i <= MLDSA_L)
58+
invariant(forall(x, 0, MLDSA_L,
59+
array_bound(v->vec[x].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
60+
{
61+
mld_poly_permute_bitrev_to_custom(v->vec[i].coeffs);
62+
}
63+
#else /* MLD_USE_NATIVE_NTT_CUSTOM_ORDER */
64+
/* Nothing to do */
65+
(void)v;
66+
#endif /* !MLD_USE_NATIVE_NTT_CUSTOM_ORDER */
67+
}
68+
3669
static void mld_polymat_permute_bitrev_to_custom(mld_polymat *mat)
3770
__contract__(
3871
/* We don't specify that this should be a permutation, but only
@@ -47,23 +80,16 @@ __contract__(
4780
array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
4881
)
4982
{
50-
#if defined(MLD_USE_NATIVE_NTT_CUSTOM_ORDER)
51-
/* TODO: proof */
52-
unsigned int i, j;
83+
unsigned int i;
5384
for (i = 0; i < MLDSA_K; i++)
85+
__loop__(
86+
assigns(i, memory_slice(mat, sizeof(mld_polymat)))
87+
invariant(i <= MLDSA_K)
88+
invariant(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L,
89+
array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))))
5490
{
55-
for (j = 0; j < MLDSA_L; j++)
56-
{
57-
mld_poly_permute_bitrev_to_custom(mat->vec[i].vec[j].coeffs);
58-
}
91+
mld_polyvecl_permute_bitrev_to_custom(&mat->vec[i]);
5992
}
60-
61-
#else /* MLD_USE_NATIVE_NTT_CUSTOM_ORDER */
62-
63-
/* Nothing to do */
64-
((void)mat);
65-
66-
#endif /* !MLD_USE_NATIVE_NTT_CUSTOM_ORDER */
6793
}
6894

6995

@@ -885,4 +911,5 @@ void mld_polyveck_unpack_t0(mld_polyveck *p,
885911
/* To facilitate single-compilation-unit (SCU) builds, undefine all macros.
886912
* Don't modify by hand -- this is auto-generated by scripts/autogen. */
887913
#undef mld_polymat_permute_bitrev_to_custom
914+
#undef mld_polyvecl_permute_bitrev_to_custom
888915
#undef mld_polyvecl_pointwise_acc_montgomery_c

‎proofs/cbmc/dummy_backend.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@
2424
#define MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4
2525
#define MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5
2626
#define MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7
27+
#define MLD_USE_NATIVE_NTT_CUSTOM_ORDER
2728

2829
#include "../../mldsa/src/native/api.h"
2930

‎proofs/cbmc/polymat_permute_bitrev_to_custom/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/polyvec.c
2121

2222
CHECK_FUNCTION_CONTRACTS=mld_polymat_permute_bitrev_to_custom
23-
USE_FUNCTION_CONTRACTS=
23+
USE_FUNCTION_CONTRACTS=mld_polyvecl_permute_bitrev_to_custom
2424
APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1
2626

‎proofs/cbmc/polyvecl_permute_bitrev_to_custom/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 = polyvecl_permute_bitrev_to_custom_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 = polyvecl_permute_bitrev_to_custom
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/polyvec.c
21+
22+
CHECK_FUNCTION_CONTRACTS=mld_polyvecl_permute_bitrev_to_custom
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 --slice-formula --no-array-field-sensitivity
30+
31+
FUNCTION_NAME = polyvecl_permute_bitrev_to_custom
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 = 12
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/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/polyvecl_permute_bitrev_to_custom/polyvecl_permute_bitrev_to_custom_harness.c‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// Copyright (c) The mldsa-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
#include "polyvec.h"
5+
6+
void mld_polyvecl_permute_bitrev_to_custom(mld_polyvecl *v);
7+
8+
void harness(void)
9+
{
10+
mld_polyvecl *v;
11+
mld_polyvecl_permute_bitrev_to_custom(v);
12+
}

‎proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/Makefile‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
# Copyright (c) The mlkem-native project authors
2+
# Copyright (c) The mldsa-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 = polyvecl_permute_bitrev_to_custom_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 = mld_polyvecl_permute_bitrev_to_custom_native
13+
14+
DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\""
15+
INCLUDES +=
16+
UNWINDSET +=
17+
18+
REMOVE_FUNCTION_BODY +=
19+
20+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
21+
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c
22+
23+
CHECK_FUNCTION_CONTRACTS=mld_polyvecl_permute_bitrev_to_custom
24+
USE_FUNCTION_CONTRACTS= mld_poly_permute_bitrev_to_custom
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=--smt2 --slice-formula --no-array-field-sensitivity
31+
32+
FUNCTION_NAME = mld_polyvecl_permute_bitrev_to_custom_native
33+
34+
# If this proof is found to consume huge amounts of RAM, you can set the
35+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
36+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
37+
# documentation in Makefile.common under the "Job Pools" heading for details.
38+
# EXPENSIVE = true
39+
CBMC_OBJECT_BITS = 10
40+
41+
# If you require access to a file-local ("static") function or object to conduct
42+
# your proof, set the following (and do not include the original source file
43+
# ("mldsa/poly.c") in PROJECT_SOURCES).
44+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
45+
# include ../Makefile.common
46+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/poly.c
47+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
48+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
49+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
50+
# be set before including Makefile.common, but any use of variables on the
51+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
52+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
53+
54+
include ../Makefile.common

‎proofs/cbmc/polyvecl_permute_bitrev_to_custom_native/polyvecl_permute_bitrev_to_custom_native_harness.c‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// Copyright (c) The mldsa-native project authors
2+
// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
3+
4+
#include "polyvec.h"
5+
6+
void mld_polyvecl_permute_bitrev_to_custom(mld_polyvecl *v);
7+
8+
void harness(void)
9+
{
10+
mld_polyvecl *v;
11+
mld_polyvecl_permute_bitrev_to_custom(v);
12+
}

‎scripts/check-contracts‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,9 @@ def gen_contracts():
4343
def is_exception(funcname):
4444
# The functions passing this filter are known not to have a proof
4545

46+
if funcname == 'poly_permute_bitrev_to_custom':
47+
return True
48+
4649
if funcname.endswith("_native") or funcname.endswith("_asm"):
4750
# CBMC proofs are axiomatized against contracts of the backends
4851
return True

0 commit comments

Comments
 (0)