Skip to content

avx2/commitment: F* proofs#874

Merged
W95Psp merged 37 commits intomainfrom
minicore-commitment-proof
Apr 23, 2025
Merged

avx2/commitment: F* proofs#874
W95Psp merged 37 commits intomainfrom
minicore-commitment-proof

Conversation

@W95Psp
Copy link
Copy Markdown
Contributor

@W95Psp W95Psp commented Mar 5, 2025 •
edited
Loading

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

hax.sh

Also, in this PR we use minicore for proofs.
Our F* models of the Rust core library and the extracted code from minicore overlap, particularly for core::arch::*.
The minicore versions offer more accurate and specialized models.

Thus, this PR also adds a utility function (see function fixup-minicore in hax.sh) that fixes up module names in a given crate: it will make the F* extraction use preferably minicore modules instead of core modules when possible.

This utility function is essentially patching files, which is trivial to do with bash. The former python script was essentially running commands.
Thus I rewrote it in bash.

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

franziskuskiefer
franziskuskiefer reviewed Mar 5, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@franziskuskiefer franziskuskiefer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

no review, just a few quick high level comments

@W95Psp W95Psp force-pushed the minicore-commitment-proof branch 2 times, most recently from 0dde429 to a3768df Compare March 12, 2025 16:09
@W95Psp W95Psp marked this pull request as ready for review March 12, 2025 16:20
@W95Psp W95Psp requested a review from a team as a code owner March 12, 2025 16:20
@W95Psp
Copy link
Copy Markdown
Contributor Author

W95Psp commented Mar 12, 2025

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

@W95Psp W95Psp requested a review from franziskuskiefer March 12, 2025 16:20
@W95Psp W95Psp requested a review from karthikbhargavan March 12, 2025 16:20
@W95Psp
Copy link
Copy Markdown
Contributor Author

W95Psp commented Mar 17, 2025

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
franziskuskiefer previously requested changes Mar 17, 2025
View reviewed changes
@W95Psp W95Psp force-pushed the minicore-commitment-proof branch from 8f106cd to af26ce9 Compare April 1, 2025 12:37
@W95Psp W95Psp mentioned this pull request Apr 1, 2025
Closed
@W95Psp W95Psp force-pushed the minicore-commitment-proof branch from 43ee877 to 1d6f757 Compare April 2, 2025 11:38
W95Psp added 15 commits April 2, 2025 13:41
@W95Psp
minicore: use hax-lib
7b4dd64
@W95Psp
minicore: replace const BITS with fn bits
e618e05 
This is required so that we can have a hax postcondition to `bits` stating it's a non-zero integer.
@W95Psp
minicore: rename core::arch to core::core_arch
ef5658b 
`core::arch` is actually `core::core_arch` in Rust's `core`.
@W95Psp
minicore: intro funarrs
3029025 
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*.
@W95Psp
libcrux-intrinsics: mark fns opaque but those provided by minicore
66c91aa
@W95Psp
libcrux-intrinsics: introduce a cfg(pre_minicore)
e07326e
@W95Psp
hax: intro hax.sh
899e0c3 
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.
@W95Psp
minicore: misc
b751e0a
@W95Psp
ml-dsa: proofs: avx2 commitment
4181d07
@W95Psp
ml-dsa: proofs: small cleanup
fccfd80
@W95Psp
gha: ml-dsa: use hax.sh instead of hax.py
6742a12
@W95Psp
ml-dsa: remove hax.py
1c11c5e
@W95Psp
mldsa: F*: remove debug
8a52644
@W95Psp
libcrux-intrinsics: F*: add precondition
571a4c2
@W95Psp
fix(ml-kem/proofs): pass cfg(pre_minicore)
3f091db
W95Psp and others added 4 commits April 9, 2025 13:02
@W95Psp @franziskuskiefer
Apply suggestions from code review
9e2f474 
Co-authored-by: Franziskus Kiefer <franziskuskiefer@gmail.com>
@W95Psp @franziskuskiefer
Update fstar-helpers/minicore/src/core_arch/x86.rs
ee152c8 
Co-authored-by: Franziskus Kiefer <franziskuskiefer@gmail.com>
@W95Psp
small cleanups
45c2262
@W95Psp
ml-dsa: proofs: don't depend on minicore unless cfg(hax)
6f87ead
@W95Psp W95Psp requested a review from franziskuskiefer April 9, 2025 13:06
@github-actions github-actions bot dismissed franziskuskiefer’s stale review April 9, 2025 13:06

Review re-requested

@W95Psp
Copy link
Copy Markdown
Contributor Author

W95Psp commented Apr 9, 2025

Thanks for you comments Karthik and Franziskus, I addressed the comments and added a comment about the F* tactic.
I should be good now (modulo bash).

@W95Psp W95Psp force-pushed the minicore-commitment-proof branch from bf21952 to b4ef45a Compare April 9, 2025 13:13
@karthikbhargavan
Copy link
Copy Markdown
Contributor

karthikbhargavan commented Apr 10, 2025

This looks good. I would like to press merge when CI is happy, so that we can get other PRs in.

@W95Psp
Copy link
Copy Markdown
Contributor Author

W95Psp commented Apr 22, 2025

@franziskuskiefer shall we merge?

@franziskuskiefer
Copy link
Copy Markdown
Member

franziskuskiefer commented Apr 23, 2025

@franziskuskiefer shall we merge?

I left another comment. This PR is pretty messy and impossible to review (5! force pushes). That's why I can't really leave an r+ here.

@W95Psp W95Psp enabled auto-merge April 23, 2025 08:59
@W95Psp W95Psp added this pull request to the merge queue Apr 23, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Apr 23, 2025
@W95Psp W95Psp enabled auto-merge April 23, 2025 14:43
@W95Psp W95Psp added this pull request to the merge queue Apr 23, 2025
Merged via the queue into main with commit 0ad6af2 Apr 23, 2025
71 checks passed
@W95Psp W95Psp deleted the minicore-commitment-proof branch April 23, 2025 15:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@franziskuskiefer franziskuskiefer franziskuskiefer left review comments

@karthikbhargavan karthikbhargavan karthikbhargavan approved these changes

Assignees

@W95Psp W95Psp

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Verifty ML-DSA: avx2/encoding/commitment: serialize_4

3 participants

@W95Psp @karthikbhargavan @franziskuskiefer