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

CBMC: Prove all fips202 functions #498

Closed
mkannwischer opened this issue Dec 4, 2024 · 0 comments · Fixed by #625
Closed

CBMC: Prove all fips202 functions #498

mkannwischer opened this issue Dec 4, 2024 · 0 comments · Fixed by #625
Labels
CBMC enhancement New feature or request
Milestone
next

Comments

@mkannwischer
Copy link
Contributor

mkannwischer commented Dec 4, 2024 •
edited by hanno-becker
Loading

Currently our CBMC proofs cover mlkem/*, axiomatizing the code in fips202/* through contracts in (see https://github.com/pq-code-package/mlkem-native/blob/main/fips202/fips202x4.h and https://github.com/pq-code-package/mlkem-native/blob/main/fips202/fips202.h.) This issue tracks the expansion of CBMC coverage to fips202/*.

I created issues for each function. This issue tracks those:
@mkannwischer mkannwischer added enhancement New feature or request CBMC labels Dec 4, 2024
@mkannwischer mkannwischer added this to the next milestone Dec 4, 2024
@mkannwischer mkannwischer mentioned this issue Jan 9, 2025
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
CBMC enhancement New feature or request
Projects
None yet
Milestone
next
Development

Successfully merging a pull request may close this issue.

CBMC: Add all Keccakx4 proofs pq-code-package/mlkem-native
2 participants
@mkannwischer @hanno-becker