Add Fast NTT and Inverse NTT for ML-KEM #95
Conversation
…ML-KEM Signed-off-by: Rod Chapman <rodchap@amazon.com>
since it is a constant for all ML-KEM variants. Moving its declaration into specification.cry also makes it a static value for the type constraint solver. Signed-off-by: Rod Chapman <rodchap@amazon.com>
Also adds properties and proofs to show that: NaiveNTT and NaiveInvNTT are inverting fast_ntt and fast_invntt are inverting NaiveNTT is equivalent to fast_ntt NaiveInvNTT is equivalent to fast_invntt Signed-off-by: Rod Chapman <rodchap@amazon.com>
rod-chapman
changed the title
…mments. Signed-off-by: Rod Chapman <rodchap@amazon.com>
There was a problem hiding this comment.
Thank you for these changes! Those are great speedups. I have a few thoughts & discussion points; the only blocking comment is adding a reference to the fast NTT algorithm.
It also looked like we needed to specifically approve CI running from external forks, I just set that to run now. We recently added a job that requires copyright notices to be added to files, which is going to fail because we historically have not added those consistently. I added some comments throughout with the correct notices, please add your email if you wish and paste those in to fix CI.
| ////////////////////////////////////////////////////////////// | ||
| // NTT "dispatcher" | ||
| // | ||
| // Here, we can choose to call either the naive or fast NTT | ||
| ////////////////////////////////////////////////////////////// | ||
|
|
||
| NTT' : Z_q_256 -> Z_q_256 | ||
| NTT' f = ParametricNTT f zeta | ||
| // fast | ||
| NTT' f = fast_ntt f | ||
| // slow | ||
| //NTT' f = NaiveNTT f | ||
|
|
||
| NTTInv' : Z_q_256 -> Z_q_256 | ||
| NTTInv' f = [term*(recip 128) | term <- ParametricNTTInv f (recip zeta)] | ||
|
|
||
| CorrectnessNTT : Z_q_256 -> Bit | ||
| property CorrectnessNTT f = NTTInv' (NTT' f) == f | ||
|
|
||
| // fast | ||
| NTTInv' f = fast_invntt f | ||
| // slow | ||
| //NTTInv' f = NaiveNTTInv f |
There was a problem hiding this comment.
thought: We've discussed internally moving away from in-code switches like this and replacing them with interfaces (but only for the case of changing parameter sizes like keys). We haven't really discussed how to approach alternative implementations of a single algorithm. I'm debating between two options:
- We could parameterize the whole file by the NTT version (fast vs slow) so it's more obvious from a user perspective (a) that there's a choice and (b) that you can choose the fast version
- We might just fix the fast version and remove the commented-out switch here. Since they're proven equivalent, I'm not sure there's any good reason for someone to choose the slow version.
There was a problem hiding this comment.
I would be happy to change that in the future to whatever coding style and policy you settle on. Can we defer that decision to another day?
There was a problem hiding this comment.
Yes, let's defer. This is not necessary for this PR, just wanted to flag it as a discussion point.
There was a problem hiding this comment.
Sounds good to me.
Signed-off-by: Rod Chapman <rodchap@amazon.com>
…ated Issue Signed-off-by: Rod Chapman <rodchap@amazon.com>
Signed-off-by: Rod Chapman <rodchap@amazon.com>
Signed-off-by: Rod Chapman <rodchap@amazon.com>
Not all of our files were committed by people at Galois.
|
Super, and thanks to everyone for their efforts and help. Can someone press the "Merge" button now?? |
This PR adds "fast" O(N log N) NTT and Inverse NTT functions for ML-KEM.
Note