Dilithium Spec

[zanxu-blackhorse]

Here is a spec for Dilithium.
We have work on a implementation as well, but wanted some feedback on this before proceeding, in order to make sure that this meets the standards and stylistic conventions of the project.

[msprotz]

Hello,

Apologies for the delay in responding, several of us were off, and it took a while to settle on a policy for external contributions. First of all, thanks very much! This is a nice piece of work and we're happy to integrate it.

Here are some high-level points... please let us know how this sounds.

• Until there is a corresponding low-level implementation, it seems wiser to leave this in specs/experimental
• Can we leave the debug helpers out of the PR for now? (same for the unused helpers at lines 123 and below of your spec test)
• One thing to agree on is maintenance. If this spec fails to verify, or breaks in the future, it's unlikely any of us will be able to fix it. What will most likely happen is that we'll add an admit() somewhere to unbreak the build, then ping one of you folks to try to fix it. If the spec remains broken for a long while, we'll almost certainly move it out to a branch to avoid having admit() in the master branch. Does that sound acceptable to you? If so, please add maybe an AUTHORS.md in specs/experimental/dilithium along with some contact info.
• We'll have to figure out how to get CI to run for your branch. We have a broken system that doesn't run CI when the PR comes from an external fork (or at least in the case of this repository, it doesn't...) so I'll have to take your branch and push it as a branch of project-everest/hacl-star. But that can happen once the points above are fixed.

As a general note, what we've seen happening is that a fresh piece of code takes a little while to stabilize, e.g. maybe there will be an F* upgrade and the code will break, which will require strengthening a proof, or improving the way a spec is crafted. This is part of the process, but a good way to avoid it would be to go over your code and try to understand why you need, e.g. fuel=2,ifuel=2,rlimit=800 and try to see if there's anything that can be done to make the files verify in a very "snappy" manner. These are specs only, so they should verify reliably and without surprisingly high rlimits... I also see a comment along the lines of "this didn't work and required a huge rlimit". Maybe debugging a little bit, adding asserts here and there to figure out which proof obligation is difficult might help figure out what's going on. As a wild guess, I would suspect some non-linear arithmetic is causing difficulties, and this might turn out to be a problem in the future.

I'm CCing @polubelova -- would you mind (once you're back from vacation of course) giving this a quick look and see if there's any potential for improvements e.g. in the way that this spec uses Lib?

Thanks,

Jonathan

[zanxu-blackhorse]

Thank you for taking the time to look at this!

Yes, I agree this is not ready for master right now. There is surely a lot of improvement that can still be done, and the rlimits are artificially higher than they need to be.
I am currently working on the low-level implementation, and have some further changes to the spec, which should clean things up.
The plan for maintenance sounds fine as well. We will add the contact info.

We may want to contribute other PQC algorithms in the future. Do you know of others currently working on F* implementations of PQC?

Thanks,
Zan

[msprotz]

@karthikbhargavan might know who else is working on post-quantum stuff -- as far as I know, we have:

• qtesla on a branch somewhere
• a very preliminary implementation of kyber sitting in a PR
• frodokem on master

that's all I'm aware of but there might be others

[karthikbhargavan]

This has been sitting around for a while and is out-of-date with master.
Is there new work in this direction that we should update with, or shall we close this PR?