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

Clean up code for fixed issues #708

Open

karthikbhargavan opened this issue Dec 5, 2024 · 0 comments

Contributor

karthikbhargavan commented Dec 5, 2024

The ML-KEM code uses some patterns to avoid bugs in hax and/or Eurydice that have since been fixed. E.g:

Fix attempted to read from stolen value hacspec/hax#27
Double return bug hacspec/hax#720
I think this one is already addressed: return values must be called "out"

We should clean these up as part of the verification effort for ML-DSA.

The text was updated successfully, but these errors were encountered:

karthikbhargavan mentioned this issue

fixing code to address review comments #705

Merged

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