CBMC: Add and prove x86_64 backend contracts #1393

willieyz · 2025-12-15T08:08:33Z

Resolves: CBMC: Prove that x86_64 backend fulfills native api.h contracts #1335
Rebased on x86_64 tomont_avx2: Remove unused qdata argument #1432, tomont isn't actually use mlk_qdata.
This PR also added proof corresponding these two hol-light: HOL-Light: Add x86 frombytes and tomont correctness proof #1418
This commit introduces CBMC verification for several x86-64 assembly functions. The contracts for these functions are derived from their corresponding HOL-Light correctness proofs.
The following functions now have CBMC proofs based on their
HOL-Light specifications:
- polyvec_basemul_acc_montgomery_cached_asm_k2/k3/k4:
  - Pre-conditions:
    <= &2 pow 12(HOL_LIGHT) v.s. MLKEM_UINT12_LIMIT + 1(CBMC)
  - Adds a CBMC pre-condition:
    requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT +
    1))
- ntt_avx2:
  - Pre-condition:
    <= &8191(HOL_LIGHT) v.s. 8191 + 1(CBMC)
  - Post-condition:
    <= &23594(HOL_LIGHT) v.s. 23594 + 1(CBMC)
  - Adds a CBMC pre-condition:
    requires(array_abs_bound(r, 0, MLKEM_N, 8192))
  - Adds a CBMC post-condition:
    ensures(array_abs_bound(r, 0, MLKEM_N, 23595))
- intt_avx2:
  - Post-condition:
    <= &26631 v.s. 26631 + 1(CBMC)
  - Adds a CBMC post-condition:
    ensures(array_abs_bound(r, 0, MLKEM_N, 26632))
- reduce_avx2:
  - Post-condition:
    < &3329(HOL_LIGHT) v.s. 3329 == MLKEM_Q(CBMC)
  - Adds a CBMC post-condition:
    ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
- tobytes_avx2:
  - Pre-condition:
    (!i. i < LENGTH l ==> val(EL i l) < 3329)(HOL_LIGHT)
    v.s.
    MLKEM_UINT12_LIMIT(CBMC)
  - Adds a CBMC pre-condition:
    requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))
- frombytes_avx2:
  - Post-conditions:
    read (memory :> bytes(a,dimindex(:32) * 12)) s0 = num_of_wordlist (l:(12 word)list)
  - Adds a CBMC post-condition:
    ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))
- mlk_rej_uniform_asm:
  - This proof are reference from aarch64 one, and change requires:
    requires(buflen % 24 == 0) to requires(buflen % 12 == 0)
- mlk_tomont_avx2:
  - Post conditions:
    (ival z_i == (tomont_3329 (ival o x)) i) (mod &3329) /\ abs(ival z_i) <= &3328)
    v.s.
    ensures(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q))
  - Add a CBMC post-condition:
    ensures(array_abs_bound(r, 0, MLKEM_N, 3328 + 1))
- mlk_poly_mulcache_compute_avx2:
  - Post conditions:
```
 read(memory :> bytes16(word_add r (word(2 * i)))) s in
              (ival zi == avx2_mulcache (ival o x) i) (mod &3329) /\
              (abs(ival zi) <= &3328))
```
    v.s.
    ensures(array_abs_bound(cache, 0, MLKEM_N/2, MLKEM_Q))
    Add a CBMC post-condition:
    ensures(array_abs_bound(out, 0, MLKEM_N/2, 3329))
- mlk_nttunpack_avx2:
  - Pre-condition:
    read(memory :> bytes(a, 512)) s = num_of_wordlist (unpermute_list l)))
    v.s.
    requires(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
  - Post-condition:
    read(memory :> bytes(a, 512)) s = num_of_wordlist (unpermute_list l)))
    v.s.
    ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
  - Add CBMC pre-condition and post-condition:
    requires(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
    ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))

mkannwischer

Thanks @willieyz - but the contracts need work. Please also make sure that the comments pointing to the specification are actually the correct files.

dev/x86_64/src/arith_native_x86_64.h

During #1393, we noticed that the HOL-Light proof for the x86 INTT proves the bound <=26632, while our contract requires <= 26631. This commit corrects the bound in the HOL-Light specification. Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer

Please also add the contract and proof for rej_uniform (#1409)

mkannwischer

Thanks @willieyz. Almost there.

dev/x86_64/src/arith_native_x86_64.h

proofs/cbmc/nttunpack_native_x86_64/Makefile

mkannwischer

Thanks @willieyz for all that work! LGTM.

@hanno-becker, please take another look.

hanno-becker · 2025-12-31T04:50:58Z

dev/x86_64/src/arith_native_x86_64.h

+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/x86/proofs/mlkem_rej_uniform.ml. */


Please add symmetric notes to all the x86 .ML proof scripts.

Hello @hanno-becker, thank you for the review.
Following your feedback, I have added symmetric notes to all .ML HOL-Light proofs that have corresponding CBMC proofs in mlkem/src/native/x86_64/src/arith_native_x86_64.h.

dev/x86_64/src/arith_native_x86_64.h

hanno-becker

This can't be completed because the HOL-Light spec for mulcache_compute is too weak. We need to fix this first.

mkannwischer · 2025-12-31T05:19:54Z

This can't be completed because the HOL-Light spec for mulcache_compute is too weak. We need to fix this first.

@willieyz, can you remove the contract and proof for mulcache_compute first, please? Please also double check that the same mistake wasn't made in the other contracts.

hanno-becker · 2025-12-31T20:53:53Z

mulcache_compute has now been fixed, so we can get the contract back in.

willieyz · 2026-01-02T08:45:45Z

mulcache_compute has now been fixed, so we can get the contract back in.

Hello, @hanno-becker , thank you for your help, I had rebase this PR on main, and add back the mulcache_compute's x86_64 backend contracts and proof

hanno-becker · 2026-01-15T15:21:15Z

dev/x86_64/src/arith_native_x86_64.h

-void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a);
+void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a)


We need to think about if/how we can capture alignment constraints.

Contrary to AArch64, 32-byte parameter alignment is mandatory for most of the AVX2 backend, and indeed part of the HOL-Light specs. However, we don't express this in the C signature, nor in the CBMC contract (and we probably can't).

hanno-becker · 2026-01-15T15:22:52Z

dev/x86_64/src/arith_native_x86_64.h

-void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a);
+void mlk_nttfrombytes_avx2(int16_t *r, const uint8_t *a)
+/* This must be kept in sync with the HOL-Light specification in
+ * proofs/hol_light/x86/proofs/mlkem_frombytes.ml.


Those paths need adjusting, it's x86_64 now

hanno-becker · 2026-01-15T15:24:14Z

mlkem/src/native/x86_64/src/arith_native_x86_64.h

+  requires(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))
+  assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+  ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))


The HOL-Light proof does not have any bounds requires/ensures clauses.

Doesn't the HOL-LIght spec say the output is a permutation of the input?
That would imply that the bounds are maintained, wouldn't it?

- This commit introduces CBMC verification for several x86-64 optimized assembly functions. The contracts for these functions are derived from their corresponding HOL-Light correctness proofs. - For each assembly function, a CBMC contract has been added to `arith_native_x86_64.h`. Additionally, new proof harnesses have been creat to formally verify that the generic C implementations (`*_native`) correctly utilize these assembly backends and adhere to the top-level API contracts. - The following functions now have CBMC proofs based on their HOL-Light specifications: - polyvec_basemul_acc_montgomery_cached_asm_k2/k3/k4: - Pre-conditions: `<= &2 pow 12`(HOL_LIGHT) v.s. `MLKEM_UINT12_LIMIT + 1`(CBMC) - Adds a CBMC pre-condition: `requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT +` `1))` - ntt_avx2: - Pre-condition: `<= &8191`(HOL_LIGHT) v.s. `8191 + 1`(CBMC) - Post-condition: `<= &23594`(HOL_LIGHT) v.s. `23594 + 1`(CBMC) - Adds a CBMC pre-condition: `requires(array_abs_bound(r, 0, MLKEM_N, 8192))` - Adds a CBMC post-condition: `ensures(array_abs_bound(r, 0, MLKEM_N, 23595))` - intt_avx2: - Post-condition: `<= &26631` v.s. `26631 + 1`(CBMC) - Adds a CBMC post-condition: `ensures(array_abs_bound(r, 0, MLKEM_N, 26632))` - reduce_avx2: - Post-condition: `< &3329`(HOL_LIGHT) v.s. `3329 == MLKEM_Q`(CBMC) - Adds a CBMC post-condition: `ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))` - tobytes_avx2: - Pre-condition: `(!i. i < LENGTH l ==> val(EL i l) < 3329)`(HOL_LIGHT) v.s. `MLKEM_UINT12_LIMIT`(CBMC) - Adds a CBMC pre-condition: `requires(array_bound(a, 0, MLKEM_N, 0, MLKEM_Q))` - frombytes_avx2: - Post-conditions: `read (memory :> bytes(a,dimindex(:32) * 12)) s0 = num_of_wordlist (l:(12 word)list)` - Adds a CBMC post-condition: `ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))` - mlk_rej_uniform_asm: - This proof are reference from aarch64 one, and change requires: `requires(buflen % 24 == 0)` to `requires(buflen % 12 == 0)` - mlk_tomont_avx2: - Post conditions: `(ival z_i == (tomont_3329 (ival o x)) i) (mod &3329) /\ abs(ival z_i) <= &3328)` v.s. `ensures(array_abs_bound(r, 0, MLKEM_N, MLKEM_Q))` - Add a CBMC post-condition: `ensures(array_abs_bound(r, 0, MLKEM_N, 3328 + 1))` - mlk_poly_mulcache_compute_avx2: - Post conditions: ``` (ival zi == avx2_mulcache (ival o x) i) (mod &3329)) /\ (abs(ival zi) <= &3328)) ``` v.s. `ensures(array_abs_bound(cache, 0, MLKEM_N/2, MLKEM_Q))` - Add a CBMC post-condition: `ensures(array_abs_bound(out, 0, MLKEM_N/2, 3329))` - mlk_nttunpack_avx2: - Pre-condition: `read(memory :> bytes(a, 512)) s = num_of_wordlist (unpermute_list l)` v.s. `requires(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))` - Post-condition: `read(memory :> bytes(a, 512)) s = num_of_wordlist (unpermute_list l)))` v.s. `ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))` - Add CBMC pre-condition and post-condition: `requires(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))` `ensures(array_bound(r, 0, MLKEM_N, 0, MLKEM_Q))` Signed-off-by: willieyz <[email protected]>

Signed-off-by: willieyz <[email protected]>

willieyz changed the title ~~Cbmc x86 backend~~ CBMC: x86-64 backend Dec 15, 2025

willieyz marked this pull request as ready for review December 15, 2025 09:23

willieyz requested a review from a team as a code owner December 15, 2025 09:23

willieyz marked this pull request as draft December 15, 2025 09:28

willieyz marked this pull request as ready for review December 15, 2025 09:28

mkannwischer requested changes Dec 15, 2025

View reviewed changes

mkannwischer marked this pull request as draft December 15, 2025 10:23

willieyz force-pushed the cbmc-x86-backend branch from 030bd4b to 348f68c Compare December 15, 2025 11:40

mkannwischer mentioned this pull request Dec 16, 2025

HOL-Light: x86 INTT output bound <=26632 -> <=26631 #1394

Closed

willieyz force-pushed the cbmc-x86-backend branch 3 times, most recently from 87acd30 to 2d3d8be Compare December 17, 2025 08:05

mkannwischer requested changes Dec 18, 2025

View reviewed changes

willieyz marked this pull request as ready for review December 18, 2025 06:32

willieyz marked this pull request as draft December 18, 2025 06:34

willieyz force-pushed the cbmc-x86-backend branch 2 times, most recently from 7229fe3 to 98b01ad Compare December 18, 2025 07:49

willieyz marked this pull request as ready for review December 18, 2025 07:55

willieyz marked this pull request as draft December 22, 2025 09:32

willieyz force-pushed the cbmc-x86-backend branch 4 times, most recently from 2b60254 to 438ad7f Compare December 23, 2025 09:12

willieyz marked this pull request as ready for review December 23, 2025 10:23

willieyz marked this pull request as ready for review December 24, 2025 11:49

mkannwischer changed the title ~~CBMC: x86-64 backend~~ CBMC: Add and prove x86_64 backend contracts Dec 25, 2025

mkannwischer requested changes Dec 25, 2025

View reviewed changes

dev/x86_64/src/arith_native_x86_64.h Outdated Show resolved Hide resolved

dev/x86_64/src/arith_native_x86_64.h Outdated Show resolved Hide resolved

proofs/cbmc/nttunpack_native_x86_64/Makefile Outdated Show resolved Hide resolved

willieyz force-pushed the cbmc-x86-backend branch 4 times, most recently from 6b47650 to 885467c Compare December 26, 2025 03:23

mkannwischer force-pushed the cbmc-x86-backend branch from 885467c to d0bd799 Compare December 27, 2025 07:02

mkannwischer approved these changes Dec 27, 2025

View reviewed changes

mkannwischer assigned hanno-becker Dec 28, 2025

hanno-becker reviewed Dec 31, 2025

View reviewed changes

dev/x86_64/src/arith_native_x86_64.h Show resolved Hide resolved

hanno-becker requested changes Dec 31, 2025

View reviewed changes

willieyz force-pushed the cbmc-x86-backend branch from 3ae93fb to 275c2b1 Compare December 31, 2025 07:38

willieyz force-pushed the cbmc-x86-backend branch 4 times, most recently from 49fdcab to 483e42f Compare January 2, 2026 06:16

willieyz requested a review from hanno-becker January 2, 2026 08:44

willieyz force-pushed the cbmc-x86-backend branch from 483e42f to 369c78a Compare January 6, 2026 05:31

hanno-becker force-pushed the cbmc-x86-backend branch from 369c78a to 6444e81 Compare January 6, 2026 11:56

hanno-becker reviewed Jan 15, 2026

View reviewed changes

willieyz added 2 commits January 16, 2026 16:03

add symmetric note to all .ML HOL-LIGHT proofs

bc7522e

Signed-off-by: willieyz <[email protected]>

willieyz force-pushed the cbmc-x86-backend branch from 6444e81 to bc7522e Compare January 16, 2026 08:03

		/* This must be kept in sync with the HOL-Light specification
		* in proofs/hol_light/x86/proofs/mlkem_rej_uniform.ml. */

		void mlk_nttfrombytes_avx2(int16_t r, const uint8_t a);
		void mlk_nttfrombytes_avx2(int16_t r, const uint8_t a)

CBMC: Add and prove x86_64 backend contracts #1393

Are you sure you want to change the base?

CBMC: Add and prove x86_64 backend contracts #1393

Conversation

willieyz commented Dec 15, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

hanno-becker Dec 31, 2025

Choose a reason for hiding this comment

Uh oh!

willieyz Dec 31, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

hanno-becker left a comment

Choose a reason for hiding this comment

Uh oh!

mkannwischer commented Dec 31, 2025

Uh oh!

hanno-becker commented Dec 31, 2025

Uh oh!

willieyz commented Jan 2, 2026

Uh oh!

hanno-becker Jan 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hanno-becker Jan 15, 2026

Choose a reason for hiding this comment

Uh oh!

hanno-becker Jan 15, 2026

Choose a reason for hiding this comment

Uh oh!

mkannwischer Jan 16, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

willieyz commented Dec 15, 2025 •

edited

Loading

hanno-becker Jan 15, 2026 •

edited

Loading