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

Add proofs for the basic functions of MLDSA arithmetic #780

Merged
merged 12 commits into from
Feb 3, 2025
Merged

Add proofs for the basic functions of MLDSA arithmetic #780

merged 12 commits into from
Feb 3, 2025

Conversation

mamonet
Copy link
Member

@mamonet mamonet commented Jan 30, 2025

This PR adds proofs for add, subtract, and get_n_least_significant_bits function for arithmetic module of ML-DSA

@mamonet mamonet requested a review from a team as a code owner January 30, 2025 09:43
karthikbhargavan
karthikbhargavan approved these changes Jan 30, 2025
View reviewed changes
Copy link
Contributor

@karthikbhargavan karthikbhargavan 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. Let's merge these functions now but let us also switch to Rust annotations in the next PR on this file, whenever possible:
See: #777

@mamonet
Copy link
Member Author

mamonet commented Jan 30, 2025

I pushed an update that provides proofs for montgomery_reduce_element() and montgomery_multiply_fe_by_fer()

@mamonet
Copy link
Member Author

mamonet commented Jan 30, 2025 •
edited
Loading

I added proofs for montgomery_multiply_by_constant() and montgomery_multiply(), I think this PR is in a good shape now. I will push proofs for the rest arithmetic functions in a different PR.

@karthikbhargavan karthikbhargavan mentioned this pull request Feb 3, 2025
Draft
@karthikbhargavan karthikbhargavan merged commit 20dc15a into main Feb 3, 2025
59 of 62 checks passed
@karthikbhargavan karthikbhargavan deleted the ml-dsa-arithmetic-basic branch February 3, 2025 15:11
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
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@mamonet @franziskuskiefer @karthikbhargavan