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

Kyber: add proofs for serialize_uncompressed_ring_element #202

Merged
merged 7 commits into from
Feb 20, 2024
Merged

Kyber: add proofs for serialize_uncompressed_ring_element #202

merged 7 commits into from
Feb 20, 2024

Conversation

W95Psp
Copy link
Collaborator

@W95Psp W95Psp commented Feb 19, 2024 •
edited

This PR:

  • introduces a BitVecEq module (we should move that to hax lib at some point, see Kyber F* extraction: move BitVecEq to hax lib #207);
  • adds a proof for the last function of the serialize module that will serve as a basis for all other proofs (which are similar) in this module;
  • fixes a regression.

@W95Psp W95Psp linked an issue Feb 19, 2024 that may be closed by this pull request
Libcrux.Kem.Kyber.Serialize.fst #165
Open
4 tasks
@W95Psp W95Psp force-pushed the lucas/serialize-proofs branch 2 times, most recently from 1a0fcb0 to 5094126 Compare February 19, 2024 11:51
@W95Psp W95Psp changed the title Kyber: add proofs for serialization functions Kyber: add proofs for serialize_uncompressed_ring_element Feb 19, 2024
@W95Psp W95Psp mentioned this pull request Feb 20, 2024
Closed
@W95Psp W95Psp mentioned this pull request Feb 20, 2024
Open
4 tasks
@W95Psp W95Psp marked this pull request as ready for review February 20, 2024 11:04
karthikbhargavan
karthikbhargavan approved these changes Feb 20, 2024
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 but yes, BitVecEq should go to rust_primitives

@W95Psp W95Psp mentioned this pull request Feb 20, 2024
Merged
@W95Psp W95Psp merged commit 795a599 into main Feb 20, 2024
15 checks passed
@W95Psp W95Psp deleted the lucas/serialize-proofs branch February 20, 2024 11:12
@W95Psp
Copy link
Collaborator Author

W95Psp commented Feb 20, 2024

(I'm not moving BitVecEq yet, because we will probably need more things in there, and I will discover that while proving the other functions, so I will do the move once everything is proven)

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

@karthikbhargavan karthikbhargavan karthikbhargavan approved these changes

Assignees
No one assigned
Labels
None yet
Projects
libcrux
Status: ✅ Done
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Libcrux.Kem.Kyber.Serialize.fst
2 participants
@W95Psp @karthikbhargavan