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 ML-DSA #594

Closed
wants to merge 426 commits into from
Closed

Lax Checking ML-DSA #594

wants to merge 426 commits into from

Conversation

karthikbhargavan
Copy link
Contributor

@karthikbhargavan karthikbhargavan commented Sep 22, 2024 •
edited
Loading

This PR extracts F* code for ML-DSA and lax-checks it.
To bypass certain F* limitations, the source Rust code is restructured in places.

karthikbhargavan and others added 30 commits August 27, 2024 14:31
@karthikbhargavan
Merge pull request #541 from cryspen/dev-ind-cca-fix
084040f 
Restoring verification for ind-cca
@W95Psp
wip
b934c24
@W95Psp
more
48fad7e
@W95Psp
Merge branch 'dev' into lf-more-serialize-proofs
e43bc13
@W95Psp
norm array_of_list
aaafdfc
@W95Psp
reduce f_elements
d1bbc2a
@karthikbhargavan
math proofs
b528d43
@mamonet
Update serialize.rs
84795a2
@karthikbhargavan
verif
3a21d67
@W95Psp
Update and improve Makefiles
e46edf3
@W95Psp
Reintroduce BitVecEq from previous proofs
0fb14cb
@W95Psp
intro tactic library to do hybrid norm/rewrite inside terms
8feb781
@W95Psp
Kill let mut, use array literal instead
47177fe
@W95Psp
Serialization pre/post in vector/traits.rs + spec in *Math.fst
77fe334
@karthikbhargavan
hax
37cab51
@karthikbhargavan
c code
7cd7a08
@W95Psp
gitignore
2e5a142
@W95Psp
intrinsics
ff0e6ad
@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
@karthikbhargavan karthikbhargavan changed the title Starting proofs for ML-DSA Arithmetic Lax Checking ML-DSA Oct 29, 2024
@karthikbhargavan karthikbhargavan marked this pull request as ready for review October 29, 2024 10:44
@karthikbhargavan karthikbhargavan changed the base branch from dev to main October 29, 2024 10:46
@karthikbhargavan karthikbhargavan marked this pull request as draft October 29, 2024 10:49
jschneider-bensch
jschneider-bensch approved these changes Oct 29, 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.

The ML-DSA Rust changes look fine to me 👍
I've just addressed some warnings about unexpected cfg(hax).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jschneider-bensch jschneider-bensch jschneider-bensch approved these changes

Assignees

@karthikbhargavan karthikbhargavan

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

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