avx2/commitment: F* proofs #874

W95Psp · 2025-03-05T16:00:51Z

This PR adds proofs by normalization for one avx2 serialization function.

(previous text)
The main problem here is libcrux-intrinsics: the avx2 proofs in ML-KEM relies on very different models.
I'm not sure what to do here: maybe I should just add a avx2_extract_minicore.rs file and add a cfg to choose between either avx2_extract or avx2_extract_minicore?
And when we migrate the ML-KEM proofs, we can kill avx2_extract.

Any opinion on that?

Fixes #886.
We'll need to file a follow up for the proof of serialize_6.

What does this PR fixes:

enables proofs with the Rust minicore
bit-level proof of serialize_4

Missing:

bit-level proof of serialize_6
higher-level statements / proofs: proofs on integers, not bit vec

This following hax PRs were created while working on this libcrux PR:

franziskuskiefer

no review, just a few quick high level comments

libcrux-ml-dsa/src/simd/avx2/encoding/commitment.rs

libcrux-ml-dsa/hax.py

libcrux-ml-dsa/Cargo.toml

franziskuskiefer · 2025-03-05T16:05:23Z

libcrux-ml-dsa/Cargo.toml

@@ -20,7 +20,8 @@ libcrux-sha3 = { version = "0.0.2-beta.3", path = "../libcrux-sha3" }
 libcrux-intrinsics = { version = "0.0.2-beta.3", path = "../libcrux-intrinsics" }
 libcrux-platform = { version = "0.0.2-beta.3", path = "../sys/platform" }
 libcrux-macros = { version = "0.0.2-beta.3", path = "../macros" }
-hax-lib = { version = "0.1.0", git = "https://github.com/hacspec/hax/"}
+hax-lib = { version = "0.1.0", git = "https://github.com/hacspec/hax/", branch = "replace-body-temp"}
+minicore = { path = "../fstar-helpers/minicore" }


So this requires releasing the minicore and actually making it releasable.

Ideally, I'd like to kill that Rust dependency. I have a plan for that but I need to experiment a little: that will require some more rewriting in F*.

So: this dependency is not needed in libcrux-intrsinsics, but I still need those in ml-dsa, but only on specs

Well, it's a dependency, so it needs to be released. path doesn't work for that.

W95Psp · 2025-03-12T16:20:15Z

I have a regression in my proof somewhere, I need to fix that.
But otherwise this PR is ready for review!

W95Psp · 2025-03-17T17:11:54Z

I fixed my proof on ML-DSA, but the proof is pretty slow. Now it's going through. Debugging is a bit long, I have to wait for F* to normalize terms before seeing actual errors. I have some ideas to speed up the proof, but I need to investigate more.

franziskuskiefer · 2025-03-17T20:05:06Z

libcrux-ml-dsa/hax.sh

Why does this need to be rewritten and what does it now?

Quoting the commit that introduces this:

@W95Psp
hax: intro hax.sh
c3c24c3

This commit introduces a hax.sh script, that aims at replacing the python script.

The script does a little more: it is fixing up core names into minicore names.

The union of modules between our hax core model (proof-libs in hax) and minicore is not empty. This is a big issue for F*.
The script thus replace references to every core module provided by minicore into a reference to the corresponding minicore module.

franziskuskiefer · 2025-03-17T20:06:36Z

libcrux-ml-dsa/Cargo.toml

@@ -20,7 +20,8 @@ libcrux-sha3 = { version = "0.0.2-beta.3", path = "../libcrux-sha3" }
 libcrux-intrinsics = { version = "0.0.2-beta.3", path = "../libcrux-intrinsics" }
 libcrux-platform = { version = "0.0.2-beta.3", path = "../sys/platform" }
 libcrux-macros = { version = "0.0.2-beta.3", path = "../macros" }
-hax-lib = { version = "0.1.0", git = "https://github.com/hacspec/hax/"}
+hax-lib = { version = "0.1.0", git = "https://github.com/hacspec/hax/", branch = "replace-body-temp"}
+minicore = { path = "../fstar-helpers/minicore" }


Well, it's a dependency, so it needs to be released. path doesn't work for that.

fstar-helpers/minicore/src/abstractions/funarr.rs

fstar-helpers/minicore/src/abstractions/bitvec.rs

franziskuskiefer · 2025-03-17T20:15:39Z

libcrux-ml-dsa/src/simd/avx2/encoding/commitment.rs

 #[inline(always)]
+fn serialize_4(simd_unit: &Vec256) -> Vec128 {


Did you check that this doesn't impact performance?

No. I am taking a look now then

Ran cargo criterion before and after applying my diff to that one file commitment.rs.
I got the following very surprising results:

Seems like the benchs are a bit flaky (as disucssed on gchat with Jonas).
Shall I inverstigate more? (if yes, how?)

Running cargo bench --bench manual65:

(seems fine, right?)

Without commitment.rs patch

(libcrux) KeyGen 65 portable: 132 μs
(libcrux) Sign 65 portable: 395 μs
(libcrux) Verify 65 portable: 123 μs

(libcrux) KeyGen 65 simd256: 130 μs
(libcrux) Sign 65 simd256: 145 μs
(libcrux) Verify 65 simd256: 53 μs

(pqclean) KeyGen 65: 41 μs
(pqclean) Sign 65: 116 μs
(pqclean) Verify 65: 45 μs

With commitment.rs patch

(libcrux) KeyGen 65 portable: 133 μs
(libcrux) Sign 65 portable: 402 μs
(libcrux) Verify 65 portable: 124 μs

(libcrux) KeyGen 65 simd256: 130 μs
(libcrux) Sign 65 simd256: 144 μs
(libcrux) Verify 65 simd256: 54 μs

(pqclean) KeyGen 65: 42 μs
(pqclean) Sign 65: 116 μs
(pqclean) Verify 65: 46 μs

Second run:

(libcrux) KeyGen 65 portable: 136 μs
(libcrux) Sign 65 portable: 394 μs
(libcrux) Verify 65 portable: 123 μs

(libcrux) KeyGen 65 simd256: 130 μs
(libcrux) Sign 65 simd256: 145 μs
(libcrux) Verify 65 simd256: 53 μs

(pqclean) KeyGen 65: 41 μs
(pqclean) Sign 65: 114 μs
(pqclean) Verify 65: 45 μs

On main branch

(libcrux) KeyGen 65 portable: 133 μs
(libcrux) Sign 65 portable: 421 μs
(libcrux) Verify 65 portable: 122 μs

(libcrux) KeyGen 65 simd256: 128 μs
(libcrux) Sign 65 simd256: 143 μs
(libcrux) Verify 65 simd256: 53 μs

(pqclean) KeyGen 65: 41 μs
(pqclean) Sign 65: 115 μs
(pqclean) Verify 65: 45 μs

This is required so that we can have a hax postcondition to `bits` stating it's a non-zero integer.

`core::arch` is actually `core::core_arch` in Rust's `core`.

This commit introduces a new abstraction: functional arrays. This is an abstraction that provides finite maps: this is useful isntead of sequences, as fun arrays extract to `->^` restricted arrows in F*. That's particularly handy for normalization in F*.

This commit introduces a `hax.sh` script, that aims at replacing the python script. The script does a little more: it is fixing up core names into minicore names. The union of modules between our hax `core` model (proof-libs in hax) and minicore is not empty. This is a big issue for F*. The script thus replace references to every core module provided by minicore into a reference to the corresponding minicore module.

libcrux-intrinsics is extracted in two different ways, depending on wether we are extracting ml-kem or ml-dsa. Thus having F* files checked in the git repo will cause troubles.

franziskuskiefer reviewed Mar 5, 2025

View reviewed changes

W95Psp force-pushed the minicore-commitment-proof branch 2 times, most recently from 0dde429 to a3768df Compare March 12, 2025 16:09

W95Psp marked this pull request as ready for review March 12, 2025 16:20

W95Psp requested a review from a team as a code owner March 12, 2025 16:20

W95Psp requested a review from franziskuskiefer March 12, 2025 16:20

W95Psp assigned karthikbhargavan and unassigned karthikbhargavan Mar 12, 2025

W95Psp requested a review from karthikbhargavan March 12, 2025 16:20

franziskuskiefer requested changes Mar 17, 2025

View reviewed changes

W95Psp added 18 commits April 1, 2025 12:36

minicore: use hax-lib

e03132c

minicore: replace const BITS with fn bits

1aa0c14

This is required so that we can have a hax postcondition to `bits` stating it's a non-zero integer.

minicore: rename core::arch to core::core_arch

18c25f2

`core::arch` is actually `core::core_arch` in Rust's `core`.

minicore: intro funarrs

1d5e533

This commit introduces a new abstraction: functional arrays. This is an abstraction that provides finite maps: this is useful isntead of sequences, as fun arrays extract to `->^` restricted arrows in F*. That's particularly handy for normalization in F*.

libcrux-intrinsics: mark fns opaque but those provided by minicore

595c774

libcrux-intrinsics: introduce a cfg(pre_minicore)

a375570

minicore: misc

13d50b4

ml-dsa: proofs: avx2 commitment

2c5404a

ml-dsa: proofs: small cleanup

98fd956

gha: ml-dsa: use hax.sh instead of hax.py

48c010d

ml-dsa: remove hax.py

a8c5fe9

libcrux-intrinsics: fstar: remove interfaces

5d8bbbc

mldsa: F*: remove debug

70bcddc

ml-dsa: refresh F* proofs

3fe0dce

libcrux-intrinsics: F*: add precondition

ca26463

fix(ml-kem/proofs): pass cfg(pre_minicore)

b3d1212

fix: add version to minicore

dddf9a2

W95Psp added 4 commits April 1, 2025 12:36

fix: inherit workspace for minicore

c5eeff3

doc(minicore): document funarr.rs

bca636f

minicore: drop comment code

c98a75e

fix(minicore): fix cargo manifest

af26ce9

W95Psp force-pushed the minicore-commitment-proof branch from 8f106cd to af26ce9 Compare April 1, 2025 12:37

proofs: intrinsics: do not check in F* proofs

43ee877

libcrux-intrinsics is extracted in two different ways, depending on wether we are extracting ml-kem or ml-dsa. Thus having F* files checked in the git repo will cause troubles.

W95Psp mentioned this pull request Apr 1, 2025

F*: drop F* files #898

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

avx2/commitment: F* proofs #874

avx2/commitment: F* proofs #874

W95Psp commented Mar 5, 2025 •

edited

Loading

franziskuskiefer left a comment

franziskuskiefer Mar 5, 2025

W95Psp Mar 6, 2025

W95Psp Mar 12, 2025

franziskuskiefer Mar 17, 2025

W95Psp commented Mar 12, 2025

W95Psp commented Mar 17, 2025

franziskuskiefer Mar 17, 2025

W95Psp Mar 18, 2025

franziskuskiefer Mar 17, 2025

franziskuskiefer Mar 17, 2025

W95Psp Apr 1, 2025

W95Psp Apr 1, 2025

W95Psp Apr 1, 2025

		#[inline(always)]
		fn serialize_4(simd_unit: &Vec256) -> Vec128 {

avx2/commitment: F* proofs #874

Are you sure you want to change the base?

avx2/commitment: F* proofs #874

Conversation

W95Psp commented Mar 5, 2025 • edited Loading

franziskuskiefer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

W95Psp commented Mar 12, 2025

W95Psp commented Mar 17, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Without commitment.rs patch

With commitment.rs patch

On main branch

W95Psp commented Mar 5, 2025 •

edited

Loading