[MLKEM] Part 1: Cross-spec tests#170
Conversation
abentkamp
force-pushed
the
alex/mlkem-verification1
branch
from
13d40c9 to
e7ebaaf
Compare
jschneider-bensch
left a comment
jschneider-bensch
left a comment
There was a problem hiding this comment.
Thanks! I have one question regarding the extraction change in SHA3, and some suggestions/questions, but I think overall this can get merged.
| pretty_env_logger = "0.5.0" | ||
| hacspec_sha3 = { git = "https://github.com/cryspen/libcrux.git", rev = "8470b57c228f12c81b27eb5abcba298729a72826" } | ||
| hacspec_sha3 = { git = "https://github.com/cryspen/libcrux.git", rev = "a4cfb1ebf26431b2ee81f0dc19383158aaf397b7" } | ||
| proptest = "1.2.0" |
There was a problem hiding this comment.
This is conflicting with the currently pinned spec. After the ML-KEM spec has been merged on mainline, can you bump this rev to the main branch merge commit for the ML-KEM spec and confirm that everything works as expected?
| @@ -362,11 +355,13 @@ pub fn shake256_ema(out: &mut [U8], data: &[U8]) { | |||
|
|
|||
| /// Incremental API for SHAKE XOFs | |||
| pub mod incremental { | |||
There was a problem hiding this comment.
Why is it necessary to exclude UnbufferedXofState from the lean extraction? As I understand it, the lean proofs for sha3-iot do not cover the incremental APIs (right?) so this shouldn't affect the proofs, correct?
| import sys | ||
| from pathlib import Path | ||
|
|
||
| HAX_VERSION = "1f85fc13b9967080cc657863e2000ba5d4aa8647" |
There was a problem hiding this comment.
It would be great to have some sort of manifest where we could pull all these revisions from in scripts like these and a checker that looks in all the places (Cargo.tomls e.g.) whether we're using the correct version from the manifest.
| with the corresponding charon/aeneas versions: | ||
| - Charon at https://github.com/AeneasVerif/charon/releases/tag/nightly-2026.06.02 | ||
| - Aeneas at https://github.com/cryspen/aeneas/releases/tag/nightly-2026.06.04 | ||
| — note: the `aeneas-pin` file in hax-evit at this commit names tag |
There was a problem hiding this comment.
Do you need to set SKIP_VERSION_CHECK=1 in your environment, then?
| result = subprocess.run(cmd, capture_output=True, text=True) | ||
| output = result.stdout + result.stderr | ||
| if expected not in output: | ||
| if os.environ.get("SKIP_VERSION_CHECK") == "1": |
There was a problem hiding this comment.
Is this used somewhere?
| // (i.e., both produce J(s, c')). | ||
| // --------------------------------------------------------------------------- | ||
|
|
||
| macro_rules! cross_spec_tests { |
There was a problem hiding this comment.
Maybe these macro definitions should live in the spec itself, since they already accept a path to an implementation module, and the top-level APIs should stay the same between iot and mainline libcrux. This way we're sure we're running the same cross-spec tests of the high level APIs between iot and mainline.
There was a problem hiding this comment.
Disregard that, actually. As seen on CI the cross-spec tests need to be adapted to the valgrind testing methodology. That is something that is not yet implemented on mainline, meaning the test code needs to look a little different between mainline and iot at the moment.
There was a problem hiding this comment.
This is the failing CI test job: https://github.com/celabshq/libcrux-iot/actions/runs/28160608636/job/83399870260
I had triggered ML-KEM tests manually to run the cross-spec tests, since they were (not yet) run on the PR itself, due to it having been stacked on a non-main branch before.
jschneider-bensch
left a comment
jschneider-bensch
left a comment
There was a problem hiding this comment.
Changing review status, due to the fixes needed for valgrind tests.
3 participants
This PR adds cross-spec tests to check that our ML-KEM implementation matches the hacspec implementation in celabshq/libcrux#1480. Since that libcrux PR uses the latest
hax-evitversion, we also upgrade the hax-evit dependency here, including the sha3 verification (This does not alter the sha3 extraction at all).TODO: There is some trouble with aeneas versions.
hax-evitpins the wrong aeneas version, and aeneas does not report its own version properly.