Skip to content

Commit 6763fe8

Browse files
willieyzmkannwischer
willieyz
authored and
mkannwischer
committed
CBMC: Add proofs on top of native functions(polyvecl_pointwise_acc_montgomery_native)
- This commit adds CBMC proofs for following the native function: `mld_polyvecl_pointwise_acc_montgomery_l4_native`, `mld_polyvecl_pointwise_acc_montgomery_l5_native` and `mld_polyvecl_pointwise_acc_montgomery_l7_native` called `polyvecl_pointwise_acc_montgomery_native`. - This following changes are include: - Apply the same harness file and construct function contract reference from `polyvecl_pointwise_acc_montgomery`. - Use the following function contracts: - `mld_polyvecl_pointwise_acc_montgomery_l4_native` - `mld_polyvecl_pointwise_acc_montgomery_l5_native` - `mld_polyvecl_pointwise_acc_montgomery_l7_native` - Add `MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4`, `MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5`, `MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7` in dummy_backend.h Signed-off-by: willieyz <willie.zhao@chelpis.com>
1 parent 788bd93 commit 6763fe8

File tree

5 files changed

+120
-6
lines changed

5 files changed

+120
-6
lines changed

‎mldsa/src/native/api.h‎

Lines changed: 42 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -504,7 +504,20 @@ __contract__(
504504
**************************************************/
505505
static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l4_native(
506506
int32_t w[MLDSA_N], const int32_t u[4][MLDSA_N],
507-
const int32_t v[4][MLDSA_N]);
507+
const int32_t v[4][MLDSA_N])
508+
__contract__(
509+
requires(memory_no_alias(w, sizeof(int32_t) * MLDSA_N))
510+
requires(memory_no_alias(u, sizeof(int32_t) * 4 * MLDSA_N))
511+
requires(memory_no_alias(v, sizeof(int32_t) * 4 * MLDSA_N))
512+
requires(forall(l0, 0, 4,
513+
array_bound(u[l0], 0, MLDSA_N, 0, MLDSA_Q)))
514+
requires(forall(l1, 0, 4,
515+
array_abs_bound(v[l1], 0, MLDSA_N, MLD_NTT_BOUND)))
516+
assigns(memory_slice(w, sizeof(int32_t) * MLDSA_N))
517+
ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS)
518+
ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(w, 0, MLDSA_N, MLDSA_Q))
519+
ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(w, MLDSA_N))
520+
);
508521
#endif /* MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4 */
509522

510523
#if defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5)
@@ -524,7 +537,20 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l4_native(
524537
**************************************************/
525538
static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l5_native(
526539
int32_t w[MLDSA_N], const int32_t u[5][MLDSA_N],
527-
const int32_t v[5][MLDSA_N]);
540+
const int32_t v[5][MLDSA_N])
541+
__contract__(
542+
requires(memory_no_alias(w, sizeof(int32_t) * MLDSA_N))
543+
requires(memory_no_alias(u, sizeof(int32_t) * 5 * MLDSA_N))
544+
requires(memory_no_alias(v, sizeof(int32_t) * 5 * MLDSA_N))
545+
requires(forall(l0, 0, 5,
546+
array_bound(u[l0], 0, MLDSA_N, 0, MLDSA_Q)))
547+
requires(forall(l1, 0, 5,
548+
array_abs_bound(v[l1], 0, MLDSA_N, MLD_NTT_BOUND)))
549+
assigns(memory_slice(w, sizeof(int32_t) * MLDSA_N))
550+
ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS)
551+
ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(w, 0, MLDSA_N, MLDSA_Q))
552+
ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(w, MLDSA_N))
553+
);
528554
#endif /* MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5 */
529555

530556
#if defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7)
@@ -544,7 +570,20 @@ static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l5_native(
544570
**************************************************/
545571
static MLD_INLINE int mld_polyvecl_pointwise_acc_montgomery_l7_native(
546572
int32_t w[MLDSA_N], const int32_t u[7][MLDSA_N],
547-
const int32_t v[7][MLDSA_N]);
573+
const int32_t v[7][MLDSA_N])
574+
__contract__(
575+
requires(memory_no_alias(w, sizeof(int32_t) * MLDSA_N))
576+
requires(memory_no_alias(u, sizeof(int32_t) * 7 * MLDSA_N))
577+
requires(memory_no_alias(v, sizeof(int32_t) * 7 * MLDSA_N))
578+
requires(forall(l0, 0, 7,
579+
array_bound(u[l0], 0, MLDSA_N, 0, MLDSA_Q)))
580+
requires(forall(l1, 0, 7,
581+
array_abs_bound(v[l1], 0, MLDSA_N, MLD_NTT_BOUND)))
582+
assigns(memory_slice(w, sizeof(int32_t) * MLDSA_N))
583+
ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS)
584+
ensures((return_value == MLD_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(w, 0, MLDSA_N, MLDSA_Q))
585+
ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged(w, MLDSA_N))
586+
);
548587
#endif /* MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7 */
549588

550589
#endif /* !MLD_NATIVE_API_H */

‎mldsa/src/polyvec.c‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -375,7 +375,6 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
375375
{
376376
#if defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4) && \
377377
MLD_CONFIG_PARAMETER_SET == 44
378-
/* TODO: proof */
379378
int ret;
380379
mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q);
381380
mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);
@@ -389,7 +388,6 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
389388
}
390389
#elif defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5) && \
391390
MLD_CONFIG_PARAMETER_SET == 65
392-
/* TODO: proof */
393391
int ret;
394392
mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q);
395393
mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);
@@ -403,7 +401,6 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
403401
}
404402
#elif defined(MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7) && \
405403
MLD_CONFIG_PARAMETER_SET == 87
406-
/* TODO: proof */
407404
int ret;
408405
mld_assert_bound_2d(u->vec, MLDSA_L, MLDSA_N, 0, MLDSA_Q);
409406
mld_assert_abs_bound_2d(v->vec, MLDSA_L, MLDSA_N, MLD_NTT_BOUND);

‎proofs/cbmc/dummy_backend.h‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,9 @@
2121
#define MLD_USE_NATIVE_POLYZ_UNPACK_17
2222
#define MLD_USE_NATIVE_POLYZ_UNPACK_19
2323
#define MLD_USE_NATIVE_POINTWISE_MONTGOMERY
24+
#define MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L4
25+
#define MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L5
26+
#define MLD_USE_NATIVE_POLYVECL_POINTWISE_ACC_MONTGOMERY_L7
2427

2528
#include "../../mldsa/src/native/api.h"
2629

‎proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/Makefile‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
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_pointwise_acc_montgomery_native_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_pointwise_acc_montgomery_native
12+
13+
DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"dummy_backend.h\""
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_NAMESPACE)polyvecl_pointwise_acc_montgomery
23+
USE_FUNCTION_CONTRACTS= mld_polyvecl_pointwise_acc_montgomery_c
24+
ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
25+
USE_FUNCTION_CONTRACTS+=mld_polyvecl_pointwise_acc_montgomery_l4_native
26+
else ifeq ($(MLD_CONFIG_PARAMETER_SET),65)
27+
USE_FUNCTION_CONTRACTS+=mld_polyvecl_pointwise_acc_montgomery_l5_native
28+
else ifeq ($(MLD_CONFIG_PARAMETER_SET),87)
29+
USE_FUNCTION_CONTRACTS+=mld_polyvecl_pointwise_acc_montgomery_l7_native
30+
endif
31+
APPLY_LOOP_CONTRACTS=on
32+
USE_DYNAMIC_FRAMES=1
33+
34+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
35+
EXTERNAL_SAT_SOLVER=
36+
CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_smt_only --z3
37+
CBMCFLAGS += --slice-formula
38+
CBMCFLAGS += --no-array-field-sensitivity
39+
40+
FUNCTION_NAME = polyvecl_pointwise_acc_montgomery_native
41+
42+
# If this proof is found to consume huge amounts of RAM, you can set the
43+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
44+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
45+
# documentation in Makefile.common under the "Job Pools" heading for details.
46+
# EXPENSIVE = true
47+
48+
# This function is large enough to need...
49+
CBMC_OBJECT_BITS = 12
50+
51+
# If you require access to a file-local ("static") function or object to conduct
52+
# your proof, set the following (and do not include the original source file
53+
# ("mldsa/poly.c") in PROJECT_SOURCES).
54+
# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
55+
# include ../Makefile.common
56+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c
57+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
58+
# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
59+
# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
60+
# be set before including Makefile.common, but any use of variables on the
61+
# left-hand side requires those variables to be defined. Hence, _SOURCE,
62+
# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
63+
64+
include ../Makefile.common

‎proofs/cbmc/polyvecl_pointwise_acc_montgomery_native/polyvecl_pointwise_acc_montgomery_native_harness.c‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
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 harness(void)
7+
{
8+
mld_poly *a;
9+
mld_polyvecl *b, *c;
10+
mld_polyvecl_pointwise_acc_montgomery(a, b, c);
11+
}

0 commit comments

Comments
 (0)