Skip to content

Commit 535dc05

Browse files
hanno-beckerhanno-becker
authored
Merge pull request #151 from pq-code-package/cbmc-polyvec-proofs
CBMC: Add contracts and proofs for various polyvec functions
2 parents 7dfed94 + 61a2040 commit 535dc05

File tree

18 files changed

+617
-18
lines changed

18 files changed

+617
-18
lines changed

‎mldsa/poly.c

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,8 @@ void poly_add(poly *c, const poly *a, const poly *b)
5050
{
5151
c->coeffs[i] = a->coeffs[i] + b->coeffs[i];
5252
}
53+
54+
cassert(forall(k, 0, MLDSA_N, c->coeffs[k] == a->coeffs[k] + b->coeffs[k]));
5355
}
5456

5557
void poly_sub(poly *c, const poly *a, const poly *b)
@@ -60,7 +62,10 @@ void poly_sub(poly *c, const poly *a, const poly *b)
6062
__loop__(
6163
invariant(i <= MLDSA_N)
6264
invariant(forall(k1, 0, i, c->coeffs[k1] == a->coeffs[k1] - b->coeffs[k1])))
63-
c->coeffs[i] = a->coeffs[i] - b->coeffs[i];
65+
{
66+
c->coeffs[i] = a->coeffs[i] - b->coeffs[i];
67+
}
68+
cassert(forall(k, 0, MLDSA_N, c->coeffs[k] == a->coeffs[k] - b->coeffs[k]));
6469
}
6570

6671
void poly_shiftl(poly *a)

‎mldsa/poly.h

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ typedef struct
2929
void poly_reduce(poly *a)
3030
__contract__(
3131
requires(memory_no_alias(a, sizeof(poly)))
32-
requires(forall(k0, 0, MLDSA_N, a->coeffs[k0] <= REDUCE_DOMAIN_MAX))
32+
requires(array_bound(a->coeffs, 0, MLDSA_N, INT32_MIN, REDUCE_DOMAIN_MAX))
3333
assigns(memory_slice(a, sizeof(poly)))
3434
ensures(array_bound(a->coeffs, 0, MLDSA_N, -REDUCE_RANGE_MAX, REDUCE_RANGE_MAX))
3535
);
@@ -68,7 +68,6 @@ __contract__(
6868
requires(memory_no_alias(b, sizeof(poly)))
6969
requires(forall(k0, 0, MLDSA_N, (int64_t) a->coeffs[k0] + b->coeffs[k0] <= INT32_MAX))
7070
requires(forall(k1, 0, MLDSA_N, (int64_t) a->coeffs[k1] + b->coeffs[k1] >= INT32_MIN))
71-
ensures(forall(k, 0, MLDSA_N, c->coeffs[k] == a->coeffs[k] + b->coeffs[k]))
7271
assigns(memory_slice(c, sizeof(poly)))
7372
);
7473

@@ -91,7 +90,6 @@ __contract__(
9190
requires(memory_no_alias(b, sizeof(poly)))
9291
requires(forall(k0, 0, MLDSA_N, (int64_t) a->coeffs[k0] - b->coeffs[k0] <= INT32_MAX))
9392
requires(forall(k1, 0, MLDSA_N, (int64_t) a->coeffs[k1] - b->coeffs[k1] >= INT32_MIN))
94-
ensures(forall(k, 0, MLDSA_N, c->coeffs[k] == a->coeffs[k] - b->coeffs[k]))
9593
assigns(memory_slice(c, sizeof(poly))));
9694

9795
#define poly_shiftl MLD_NAMESPACE(poly_shiftl)

‎mldsa/polyvec.c

Lines changed: 56 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -65,8 +65,18 @@ void polyvecl_reduce(polyvecl *v)
6565
unsigned int i;
6666

6767
for (i = 0; i < MLDSA_L; ++i)
68+
__loop__(
69+
invariant(i <= MLDSA_L)
70+
invariant(forall(k0, i, MLDSA_L, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1])))
71+
invariant(forall(k2, 0, i,
72+
array_bound(v->vec[k2].coeffs, 0, MLDSA_N, -REDUCE_RANGE_MAX, REDUCE_RANGE_MAX))))
6873
{
69-
poly_reduce(&v->vec[i]);
74+
poly t = v->vec[i];
75+
poly_reduce(&t);
76+
/* Full struct assignment from local variables to simplify proof */
77+
/* TODO: eliminate once CBMC resolves
78+
* https://github.com/diffblue/cbmc/issues/8617 */
79+
v->vec[i] = t;
7080
}
7181
}
7282

@@ -75,8 +85,15 @@ void polyvecl_add(polyvecl *w, const polyvecl *u, const polyvecl *v)
7585
unsigned int i;
7686

7787
for (i = 0; i < MLDSA_L; ++i)
88+
__loop__(
89+
invariant(i <= MLDSA_L))
7890
{
79-
poly_add(&w->vec[i], &u->vec[i], &v->vec[i]);
91+
poly t;
92+
poly_add(&t, &u->vec[i], &v->vec[i]);
93+
/* Full struct assignment from local variables to simplify proof */
94+
/* TODO: eliminate once CBMC resolves
95+
* https://github.com/diffblue/cbmc/issues/8617 */
96+
w->vec[i] = t;
8097
}
8198
}
8299

@@ -161,8 +178,19 @@ void polyveck_reduce(polyveck *v)
161178
unsigned int i;
162179

163180
for (i = 0; i < MLDSA_K; ++i)
181+
__loop__(
182+
invariant(i <= MLDSA_K)
183+
invariant(forall(k0, i, MLDSA_K, forall(k1, 0, MLDSA_N, v->vec[k0].coeffs[k1] == loop_entry(*v).vec[k0].coeffs[k1])))
184+
invariant(forall(k2, 0, i,
185+
array_bound(v->vec[k2].coeffs, 0, MLDSA_N, -REDUCE_RANGE_MAX, REDUCE_RANGE_MAX)))
186+
)
164187
{
165-
poly_reduce(&v->vec[i]);
188+
poly t = v->vec[i];
189+
poly_reduce(&t);
190+
/* Full struct assignment from local variables to simplify proof */
191+
/* TODO: eliminate once CBMC resolves
192+
* https://github.com/diffblue/cbmc/issues/8617 */
193+
v->vec[i] = t;
166194
}
167195
}
168196

@@ -181,8 +209,15 @@ void polyveck_add(polyveck *w, const polyveck *u, const polyveck *v)
181209
unsigned int i;
182210

183211
for (i = 0; i < MLDSA_K; ++i)
212+
__loop__(
213+
invariant(i <= MLDSA_K))
184214
{
185-
poly_add(&w->vec[i], &u->vec[i], &v->vec[i]);
215+
poly t;
216+
poly_add(&t, &u->vec[i], &v->vec[i]);
217+
/* Full struct assignment from local variables to simplify proof */
218+
/* TODO: eliminate once CBMC resolves
219+
* https://github.com/diffblue/cbmc/issues/8617 */
220+
w->vec[i] = t;
186221
}
187222
}
188223

@@ -191,8 +226,16 @@ void polyveck_sub(polyveck *w, const polyveck *u, const polyveck *v)
191226
unsigned int i;
192227

193228
for (i = 0; i < MLDSA_K; ++i)
229+
__loop__(
230+
assigns(i, object_whole(w))
231+
invariant(i <= MLDSA_K))
194232
{
195-
poly_sub(&w->vec[i], &u->vec[i], &v->vec[i]);
233+
poly t;
234+
poly_sub(&t, &u->vec[i], &v->vec[i]);
235+
/* Full struct assignment from local variables to simplify proof */
236+
/* TODO: eliminate once CBMC resolves
237+
* https://github.com/diffblue/cbmc/issues/8617 */
238+
w->vec[i] = t;
196239
}
197240
}
198241

@@ -311,8 +354,15 @@ void polyveck_use_hint(polyveck *w, const polyveck *u, const polyveck *h)
311354
unsigned int i;
312355

313356
for (i = 0; i < MLDSA_K; ++i)
357+
__loop__(
358+
invariant(i <= MLDSA_K))
314359
{
315-
poly_use_hint(&w->vec[i], &u->vec[i], &h->vec[i]);
360+
poly t;
361+
poly_use_hint(&t, &u->vec[i], &h->vec[i]);
362+
/* Full struct assignment from local variables to simplify proof */
363+
/* TODO: eliminate once CBMC resolves
364+
* https://github.com/diffblue/cbmc/issues/8617 */
365+
w->vec[i] = t;
316366
}
317367
}
318368

‎mldsa/polyvec.h

Lines changed: 105 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,24 @@ void polyvecl_uniform_gamma1(polyvecl *v, const uint8_t seed[MLDSA_CRHBYTES],
2525
uint16_t nonce);
2626

2727
#define polyvecl_reduce MLD_NAMESPACE(polyvecl_reduce)
28-
void polyvecl_reduce(polyvecl *v);
28+
/*************************************************
29+
* Name: polyvecl_reduce
30+
*
31+
* Description: Inplace reduction of all coefficients of all polynomial in a
32+
* vector of length MLDSA_L to
33+
* representative in [-6283008,6283008].
34+
*
35+
* Arguments: - poly *v: pointer to input/output vector
36+
**************************************************/
37+
void polyvecl_reduce(polyvecl *v)
38+
__contract__(
39+
requires(memory_no_alias(v, sizeof(polyvecl)))
40+
requires(forall(k0, 0, MLDSA_L,
41+
array_bound(v->vec[k0].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE_DOMAIN_MAX)))
42+
assigns(memory_slice(v, sizeof(polyvecl)))
43+
ensures(forall(k1, 0, MLDSA_L,
44+
array_bound(v->vec[k1].coeffs, 0, MLDSA_N, -REDUCE_RANGE_MAX, REDUCE_RANGE_MAX)))
45+
);
2946

3047
#define polyvecl_add MLD_NAMESPACE(polyvecl_add)
3148
/*************************************************
@@ -38,7 +55,17 @@ void polyvecl_reduce(polyvecl *v);
3855
* - const polyvecl *u: pointer to first summand
3956
* - const polyvecl *v: pointer to second summand
4057
**************************************************/
41-
void polyvecl_add(polyvecl *w, const polyvecl *u, const polyvecl *v);
58+
void polyvecl_add(polyvecl *w, const polyvecl *u, const polyvecl *v)
59+
__contract__(
60+
requires(memory_no_alias(w, sizeof(polyvecl)))
61+
requires(memory_no_alias(u, sizeof(polyvecl)))
62+
requires(memory_no_alias(v, sizeof(polyvecl)))
63+
requires(forall(k0, 0, MLDSA_L,
64+
forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] + v->vec[k0].coeffs[k1] <= INT32_MAX)))
65+
requires(forall(k2, 0, MLDSA_L,
66+
forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] + v->vec[k2].coeffs[k3] >= INT32_MIN)))
67+
assigns(memory_slice(w, sizeof(polyvecl)))
68+
);
4269

4370
#define polyvecl_ntt MLD_NAMESPACE(polyvecl_ntt)
4471
/*************************************************
@@ -109,7 +136,16 @@ void polyveck_uniform_eta(polyveck *v, const uint8_t seed[MLDSA_CRHBYTES],
109136
*
110137
* Arguments: - polyveck *v: pointer to input/output vector
111138
**************************************************/
112-
void polyveck_reduce(polyveck *v);
139+
void polyveck_reduce(polyveck *v)
140+
__contract__(
141+
requires(memory_no_alias(v, sizeof(polyveck)))
142+
requires(forall(k0, 0, MLDSA_K,
143+
array_bound(v->vec[k0].coeffs, 0, MLDSA_N, INT32_MIN, REDUCE_DOMAIN_MAX)))
144+
assigns(memory_slice(v, sizeof(polyveck)))
145+
ensures(forall(k1, 0, MLDSA_K,
146+
array_bound(v->vec[k1].coeffs, 0, MLDSA_N, -REDUCE_RANGE_MAX, REDUCE_RANGE_MAX)))
147+
);
148+
113149
#define polyveck_caddq MLD_NAMESPACE(polyveck_caddq)
114150
/*************************************************
115151
* Name: polyveck_caddq
@@ -132,7 +168,19 @@ void polyveck_caddq(polyveck *v);
132168
* - const polyveck *u: pointer to first summand
133169
* - const polyveck *v: pointer to second summand
134170
**************************************************/
135-
void polyveck_add(polyveck *w, const polyveck *u, const polyveck *v);
171+
void polyveck_add(polyveck *w, const polyveck *u, const polyveck *v)
172+
__contract__(
173+
requires(memory_no_alias(w, sizeof(polyveck)))
174+
requires(memory_no_alias(u, sizeof(polyveck)))
175+
requires(memory_no_alias(v, sizeof(polyveck)))
176+
requires(forall(k0, 0, MLDSA_K,
177+
forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] + v->vec[k0].coeffs[k1] <= INT32_MAX)))
178+
requires(forall(k2, 0, MLDSA_K,
179+
forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] + v->vec[k2].coeffs[k3] >= INT32_MIN)))
180+
assigns(memory_slice(w, sizeof(polyveck)))
181+
);
182+
183+
#define polyveck_sub MLD_NAMESPACE(polyveck_sub)
136184
/*************************************************
137185
* Name: polyveck_sub
138186
*
@@ -144,8 +192,18 @@ void polyveck_add(polyveck *w, const polyveck *u, const polyveck *v);
144192
* - const polyveck *v: pointer to second input vector to be
145193
* subtracted from first input vector
146194
**************************************************/
147-
#define polyveck_sub MLD_NAMESPACE(polyveck_sub)
148-
void polyveck_sub(polyveck *w, const polyveck *u, const polyveck *v);
195+
void polyveck_sub(polyveck *w, const polyveck *u, const polyveck *v)
196+
__contract__(
197+
requires(memory_no_alias(w, sizeof(polyveck)))
198+
requires(memory_no_alias(u, sizeof(polyveck)))
199+
requires(memory_no_alias(v, sizeof(polyveck)))
200+
requires(forall(k0, 0, MLDSA_K,
201+
forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] - v->vec[k0].coeffs[k1] <= INT32_MAX)))
202+
requires(forall(k2, 0, MLDSA_K,
203+
forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] - v->vec[k2].coeffs[k3] >= INT32_MIN)))
204+
assigns(memory_slice(w, sizeof(polyveck)))
205+
);
206+
149207
#define polyveck_shiftl MLD_NAMESPACE(polyveck_shiftl)
150208
/*************************************************
151209
* Name: polyveck_shiftl
@@ -278,11 +336,50 @@ __contract__(
278336
* - const polyveck *u: pointer to input vector
279337
* - const polyveck *h: pointer to input hint vector
280338
**************************************************/
281-
void polyveck_use_hint(polyveck *w, const polyveck *v, const polyveck *h);
339+
void polyveck_use_hint(polyveck *w, const polyveck *v, const polyveck *h)
340+
__contract__(
341+
requires(memory_no_alias(w, sizeof(polyveck)))
342+
requires(memory_no_alias(v, sizeof(polyveck)))
343+
requires(memory_no_alias(h, sizeof(polyveck)))
344+
requires(forall(k0, 0, MLDSA_K,
345+
array_bound(v->vec[k0].coeffs, 0, MLDSA_N, 0, MLDSA_Q)))
346+
requires(forall(k1, 0, MLDSA_K,
347+
array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
348+
assigns(memory_slice(w, sizeof(polyveck)))
349+
requires(forall(k2, 0, MLDSA_K,
350+
array_bound(w->vec[k2].coeffs, 0, MLDSA_N, 0, (MLDSA_Q-1)/(2*MLDSA_GAMMA2))))
351+
);
282352

283353
#define polyveck_pack_w1 MLD_NAMESPACE(polyveck_pack_w1)
354+
/*************************************************
355+
* Name: polyveck_pack_w1
356+
*
357+
* Description: Bit-pack polynomial vector w1 with coefficients in [0,15] or
358+
* [0,43].
359+
* Input coefficients are assumed to be standard representatives.
360+
*
361+
* Arguments: - uint8_t *r: pointer to output byte array with at least
362+
* MLDSA_K* MLDSA_POLYW1_PACKEDBYTES bytes
363+
* - const polyveck *a: pointer to input polynomial vector
364+
**************************************************/
284365
void polyveck_pack_w1(uint8_t r[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES],
285-
const polyveck *w1);
366+
const polyveck *w1)
367+
#if MLDSA_MODE == 2
368+
__contract__(
369+
requires(memory_no_alias(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES))
370+
requires(memory_no_alias(w1, sizeof(polyveck)))
371+
requires(forall(k1, 0, MLDSA_K,
372+
array_bound(w1->vec[k1].coeffs, 0, MLDSA_N, 0, 44)))
373+
assigns(object_whole(r)));
374+
#else /* MLDSA_MODE == 2 */
375+
__contract__(
376+
requires(memory_no_alias(r, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES))
377+
requires(memory_no_alias(w1, sizeof(polyveck)))
378+
requires(forall(k1, 0, MLDSA_K,
379+
array_bound(w1->vec[k1].coeffs, 0, MLDSA_N, 0, 16)))
380+
assigns(object_whole(r)));
381+
#endif /* MLDSA_MODE != 2 */
382+
286383

287384
#define polyveck_pack_eta MLD_NAMESPACE(polyveck_pack_eta)
288385
void polyveck_pack_eta(uint8_t r[MLDSA_K * MLDSA_POLYETA_PACKEDBYTES],

‎proofs/cbmc/polyveck_add/Makefile

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
# SPDX-License-Identifier: Apache-2.0
2+
3+
include ../Makefile_params.common
4+
5+
HARNESS_ENTRY = harness
6+
HARNESS_FILE = polyveck_add_harness
7+
8+
# This should be a unique identifier for this proof, and will appear on the
9+
# Litani dashboard. It can be human-readable and contain spaces if you wish.
10+
PROOF_UID = polyveck_add
11+
12+
DEFINES +=
13+
INCLUDES +=
14+
15+
REMOVE_FUNCTION_BODY +=
16+
UNWINDSET +=
17+
18+
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
19+
PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c
20+
21+
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_add
22+
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_add
23+
APPLY_LOOP_CONTRACTS=on
24+
USE_DYNAMIC_FRAMES=1
25+
26+
# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
27+
EXTERNAL_SAT_SOLVER=
28+
CBMCFLAGS=--smt2
29+
30+
FUNCTION_NAME = polyveck_add
31+
32+
# If this proof is found to consume huge amounts of RAM, you can set the
33+
# EXPENSIVE variable. With new enough versions of the proof tools, this will
34+
# restrict the number of EXPENSIVE CBMC jobs running at once. See the
35+
# documentation in Makefile.common under the "Job Pools" heading for details.
36+
# EXPENSIVE = true
37+
38+
# This function is large enough to need...
39+
CBMC_OBJECT_BITS = 8
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/polyveck_add/polyveck_add_harness.c

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

0 commit comments

Comments
 (0)