Skip to content

Commit 610ceb0

Browse files
hanno-beckerhanno-becker
committed
CBMC: Simplify specification for native basemul implementations
Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
1 parent 5c38b38 commit 610ceb0

File tree

7 files changed

+18
-45
lines changed

7 files changed

+18
-45
lines changed

‎dev/aarch64_clean/src/arith_native_aarch64.h‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ __contract__(
6363
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
6464
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
6565
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
66-
requires(array_bound(a, 0, 2 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
66+
requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
6767
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
6868
);
6969

@@ -81,7 +81,7 @@ __contract__(
8181
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
8282
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
8383
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
84-
requires(array_bound(a, 0, 3 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
84+
requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
8585
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
8686
);
8787

@@ -99,7 +99,7 @@ __contract__(
9999
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
100100
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
101101
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
102-
requires(array_bound(a, 0, 4 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
102+
requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
103103
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
104104
);
105105

‎dev/aarch64_opt/src/arith_native_aarch64.h‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ __contract__(
6363
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
6464
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
6565
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
66-
requires(array_bound(a, 0, 2 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
66+
requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
6767
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
6868
);
6969

@@ -81,7 +81,7 @@ __contract__(
8181
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
8282
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
8383
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
84-
requires(array_bound(a, 0, 3 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
84+
requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
8585
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
8686
);
8787

@@ -99,7 +99,7 @@ __contract__(
9999
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
100100
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
101101
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
102-
requires(array_bound(a, 0, 4 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
102+
requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
103103
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
104104
);
105105

‎mlkem/native/aarch64/src/arith_native_aarch64.h‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ __contract__(
6363
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
6464
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
6565
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
66-
requires(array_bound(a, 0, 2 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
66+
requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
6767
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
6868
);
6969

@@ -81,7 +81,7 @@ __contract__(
8181
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
8282
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
8383
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
84-
requires(array_bound(a, 0, 3 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
84+
requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
8585
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
8686
);
8787

@@ -99,7 +99,7 @@ __contract__(
9999
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
100100
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
101101
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
102-
requires(array_bound(a, 0, 4 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
102+
requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
103103
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
104104
);
105105

‎mlkem/native/api.h‎

Lines changed: 3 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -242,17 +242,7 @@ __contract__(
242242
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
243243
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
244244
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
245-
/* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
246-
* just use a single flattened array_bound(...) here.
247-
*
248-
* Once fixed, change to:
249-
* ```
250-
* requires(array_bound(a, 0, 2 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
251-
* ```
252-
*/
253-
requires(forall(kN, 0, 2, \
254-
array_bound(&((int16_t(*)[MLKEM_N])(a))[kN][0], 0, MLKEM_N, \
255-
0, MLKEM_UINT12_LIMIT)))
245+
requires(array_bound(a, 0, 2 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
256246
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
257247
);
258248
#endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 2 */
@@ -285,17 +275,7 @@ __contract__(
285275
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
286276
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
287277
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
288-
/* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
289-
* just use a single flattened array_bound(...) here.
290-
*
291-
* Once fixed, change to:
292-
* ```
293-
* requires(array_bound(a, 0, 3 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
294-
* ```
295-
*/
296-
requires(forall(kN, 0, 3, \
297-
array_bound(&((int16_t(*)[MLKEM_N])(a))[kN][0], 0, MLKEM_N, \
298-
0, MLKEM_UINT12_LIMIT)))
278+
requires(array_bound(a, 0, 3 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
299279
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
300280
);
301281
#endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 3 */
@@ -328,17 +308,7 @@ __contract__(
328308
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
329309
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
330310
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
331-
/* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
332-
* just use a single flattened array_bound(...) here.
333-
*
334-
* Once fixed, change to:
335-
* ```
336-
* requires(array_bound(a, 0, 4 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
337-
* ```
338-
*/
339-
requires(forall(kN, 0, 4, \
340-
array_bound(&((int16_t(*)[MLKEM_N])(a))[kN][0], 0, MLKEM_N, \
341-
0, MLKEM_UINT12_LIMIT)))
311+
requires(array_bound(a, 0, 4 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
342312
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
343313
);
344314
#endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 4 */

‎proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -378,7 +378,8 @@ let poly_basemul_acc_montgomery_cached_k2_SPEC = prove(poly_basemul_acc_montgome
378378
CONV_TAC INT_RING
379379
);;
380380

381-
(* NOTE: This needs to be kept in sync with the CBMC spec in native/api.h *)
381+
(* NOTE: This needs to be kept in sync with the CBMC spec in
382+
* mlkem/native/aarch64/src/arith_native_aarch64.h *)
382383
let poly_basemul_acc_montgomery_cached_k2_SPEC' = prove(
383384
`forall srcA srcB srcBt dst x0 y0 y0t x1 y1 y1t pc returnaddress stackpointer.
384385
aligned 16 stackpointer /\

‎proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -442,7 +442,8 @@ let basemul3_odd = define
442442
CONV_TAC INT_RING
443443
);;
444444

445-
(* NOTE: This needs to be kept in sync with the CBMC spec in native/api.h *)
445+
(* NOTE: This needs to be kept in sync with the CBMC spec in
446+
* mlkem/native/aarch64/src/arith_native_aarch64.h *)
446447
let poly_basemul_acc_montgomery_cached_k3_SPEC' = prove(
447448
`forall srcA srcB srcBt dst x0 y0 y0t x1 y1 y1t x2 y2 y2t pc returnaddress stackpointer.
448449
aligned 16 stackpointer /\

‎proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -508,7 +508,8 @@ let basemul4_odd = define
508508
CONV_TAC INT_RING
509509
);;
510510

511-
(* NOTE: This needs to be kept in sync with the CBMC spec in native/api.h *)
511+
(* NOTE: This needs to be kept in sync with the CBMC spec in
512+
* mlkem/native/aarch64/src/arith_native_aarch64.h *)
512513
let poly_basemul_acc_montgomery_cached_k4_SPEC' = prove(
513514
`forall srcA srcB srcBt dst x0 y0 y0t x1 y1 y1t x2 y2 y2t x3 y3 y3t pc returnaddress stackpointer.
514515
aligned 16 stackpointer /\

0 commit comments

Comments
 (0)