Skip to content

CBMC: Refine bounds for input and output of base multiplication #906

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 11 commits into
base: main
Choose a base branch
from
Draft

CBMC: Refine bounds for input and output of base multiplication #906

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
f18ce9f
Switch mlk_polyvec and mlk_polymat to struct wrappers
hanno-becker Nov 2, 2025
9561e1e
Switch mlk_polyvec and mlk_polymat to struct wrappers
hanno-becker Jul 9, 2025
dbd46a3
CBMC: Refine bounds for input and output of base multiplication
hanno-becker Mar 24, 2025
1e4a6ce
Use --arrays-uf-always here to improve proof speed.
rod-chapman Jun 9, 2025
fe70de2
Fix merge conflicts and complete rebase again main branch.
rod-chapman Oct 7, 2025
d3d1e9c
Use C90 comments /* */ not C99 // style.
rod-chapman Oct 7, 2025
695acb0
Update component testing code for new type signatures.
rod-chapman Oct 7, 2025
ec4fd6d
Re-generate auto-generated files to meet lint requirements.
rod-chapman Oct 7, 2025
2a8542f
Update post-condition on native implementions of
rod-chapman Oct 7, 2025
44ba045
Update master copies of AArch64 arithmetic back-end specs.
rod-chapman Oct 7, 2025
bdd712e
Merge branch 'structured' into refine_bounds
rod-chapman Nov 4, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions dev/aarch64_clean/src/arith_native_aarch64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,13 +117,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
*/
/* TODO - refine_bounds branch - Check HOL-Light specification has the
* INT16_MAX/2 bound on post-condition and re-prove/
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
Expand All @@ -134,13 +138,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
*/
/* TODO - refine_bounds branch - Check HOL-Light specification has the
* INT16_MAX/2 bound on post-condition and re-prove/
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
Expand All @@ -151,13 +159,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
*/
/* TODO - refine_bounds branch - Check HOL-Light specification has the
* INT16_MAX/2 bound on post-condition and re-prove/
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);

#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
Expand Down
12 changes: 12 additions & 0 deletions dev/aarch64_opt/src/arith_native_aarch64.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -116,13 +116,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
*/
/* TODO - refine_bounds branch - Check HOL-Light specification has the
* INT16_MAX/2 bound on post-condition and re-prove/
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
Expand All @@ -133,13 +137,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
*/
/* TODO - refine_bounds branch - Check HOL-Light specification has the
* INT16_MAX/2 bound on post-condition and re-prove/
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);

#define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
Expand All @@ -150,13 +158,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(
/* This must be kept in sync with the HOL-Light specification in
* proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
*/
/* TODO - refine_bounds branch - Check HOL-Light specification has the
* INT16_MAX/2 bound on post-condition and re-prove/
*/
__contract__(
requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
);

#define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
Expand Down
Loading
Loading