Skip to content
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

Jump to bottom

Lax Checking for ML-DSA #646

Merged
merged 444 commits into from
Nov 5, 2024
Merged

Lax Checking for ML-DSA #646

merged 444 commits into from
Nov 5, 2024

Conversation

karthikbhargavan
Copy link
Contributor

This PR adds lax-checking for ML-DSA

W95Psp and others added 30 commits August 30, 2024 21:42
@W95Psp
partial proofs
bfeeda3
@W95Psp
avx2: serialize: manual proofs
7c4e54b
@W95Psp
portable: serialize: manual proofs
dd063cc
@W95Psp
makefile, more fixes
64a2732
@karthikbhargavan
c code
bab1d08
@karthikbhargavan
Merge pull request #548 from cryspen/dev-bounded-poly
8d9d191 
Arithmetic proofs
@karthikbhargavan
stabilize ind-cca
0de2f94
@karthikbhargavan
Merge branch 'dev' into dev-arithmetic-proofs
a5eeb0b
@karthikbhargavan
arith
bc45818
@karthikbhargavan
portable/arithmetic
7b03687
@karthikbhargavan
avx2 arithmetic
b6cb1c4
@mamonet
Add lemmas for Portable serialize/deserialize functions
8a8e806
@mamonet
Comment out pre/post-conditions for serialize fun in vector/traits.rs
ea8f110
@mamonet
Fix return array in serialize_1
c8b2d7e
@mamonet
Fix fstar::replace for mm256_srli_epi16
3635503
@mamonet
Update extracted F* files for intrinsics and ml-kem
10b4615
@karthikbhargavan
wip
89af067
@karthikbhargavan
wip
133225f
@karthikbhargavan
verifying
56eed0a
@karthikbhargavan
Merge pull request #550 from cryspen/lf-more-serilize-proofs-2
ec6b25a 
Add lemmas for Portable serialize/deserialize functions
@karthikbhargavan
fmt
aa003c8
@karthikbhargavan
fstar feat
87ab89d
@karthikbhargavan
Merge pull request #549 from cryspen/lf-tactics-serialize
db6b548 
Tactics for serialize
@karthikbhargavan
arithmetic
894d5ee
@karthikbhargavan
wip
11c8589
@karthikbhargavan
Merge branch 'dev' into vector-spec-sampling-pf
33d08ed
@mamonet
Use z3refresh on tactic calls for serialize.rs
0ad4043
@W95Psp
makefile: add a SLOW_MODULES variable
37d4f52
@karthikbhargavan
refreshed c code
61a2488
@karthikbhargavan
new eurydice_glue
38c246d
jschneider-bensch
jschneider-bensch previously requested changes Oct 30, 2024
View reviewed changes
Copy link
Collaborator

@jschneider-bensch jschneider-bensch left a comment

Choose a reason for hiding this comment

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

Looks good, just some small things / questions.

Cargo.toml Outdated Show resolved Hide resolved
libcrux-ml-dsa/src/hash_functions.rs Outdated Show resolved Hide resolved
libcrux-ml-dsa/src/simd/portable/arithmetic.rs Show resolved Hide resolved
libcrux-ml-dsa/src/ml_dsa_generic.rs Outdated Show resolved Hide resolved
franziskuskiefer
franziskuskiefer previously requested changes Nov 1, 2024
View reviewed changes
Copy link
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.

Generally looks ok. Some unfortunate changes.
But most of them are ok with a few comments on them.

And we need to synchronise with #642 as both are touching a lot of code in ML-DSA.

.gitignore Show resolved Hide resolved
Cargo.toml Outdated Show resolved Hide resolved
benchmarks/benches/kyber768.rs Show resolved Hide resolved
libcrux-ml-dsa/hax.py Show resolved Hide resolved
libcrux-ml-dsa/src/arithmetic.rs Show resolved Hide resolved
libcrux-ml-dsa/src/ntt.rs Show resolved Hide resolved
libcrux-ml-dsa/src/simd/portable/vector_type.rs Outdated Show resolved Hide resolved
libcrux-ml-dsa/src/simd/portable/ntt.rs Show resolved Hide resolved
libcrux-ml-dsa/src/simd/portable/encoding/t0.rs Show resolved Hide resolved
libcrux-ml-dsa/src/simd/avx2/ntt.rs Show resolved Hide resolved
franziskuskiefer
franziskuskiefer requested changes Nov 4, 2024
View reviewed changes
Copy link
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.

There are bunch of comments that haven't been addressed yet.

franziskuskiefer
franziskuskiefer approved these changes Nov 5, 2024
View reviewed changes
Copy link
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.

Let's get this in.

@franziskuskiefer franziskuskiefer added this pull request to the merge queue Nov 5, 2024
Merged via the queue into main with commit 5ddbf9e Nov 5, 2024
50 checks passed
@franziskuskiefer franziskuskiefer deleted the ml-dsa-lax branch November 5, 2024 11:42
@franziskuskiefer franziskuskiefer mentioned this pull request Nov 6, 2024
Closed
@franziskuskiefer franziskuskiefer mentioned this pull request Nov 15, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@W95Psp W95Psp W95Psp left review comments

@franziskuskiefer franziskuskiefer franziskuskiefer approved these changes

@jschneider-bensch jschneider-bensch Awaiting requested review from jschneider-bensch

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@karthikbhargavan @W95Psp @franziskuskiefer @jschneider-bensch @mamonet @maximebuyse