Add Keccak (SHA-3)

[xrchz]

Formalises the NIST Standard that defines SHA-3. There is room for improvement in EVAL-uation of the algorithms, but the specification is defined and there is an sptree-based EVAL-able version. Two example theorems are used to establish that there is agreement with well-known hash values.

[mn200]

Please:

• add the directory to src/parallel_builds/core/Holmakefile under an appropriate selftest level
• remove this script's development of chunks given it's now part of rich_list
• [maybe] move the tests from the end of the file into a separate selftest.sml file

[xrchz]

I think I've done the first two bullets. The comments at the end of the file aren't really selftest material - more like debugging... I could delete it, or maybe leave it for future when moving towards the cvcompute version? I think at that point the eval stuff should also move into a separate reusable lib. But for now the actual tests are just the theorems computing hashes of the empty string.

[mn200]

Thanks for this!

[binghe]

Hi, how long it usually takes to build this keccakTheory?

Yesterday I tried to build it with the experimental kernel (--expk) and after 9 hours it's still not finished (the last exported theorem is rho_spt_100_example, so it's in proving the next one, Keccak_224_NIL). Then today I just tried with standard kernel on unmodified develop, the last two theorems (Keccak_224_NIL and Keccak_256_NIL) took most of the time, but at least Keccak_224_NIL finished in about 10 minutes.

[mn200]

Interesting! On my MBP, with the standard kernel, the whole script took 14m32s, with the bulk of that being taken up by the very last EVAL (the 256-NIL). I will adjust the build sequence to maybe make this directory standard kernel only.

[binghe]

Interesting! On my MBP, with the standard kernel, the whole script took 14m32s, with the bulk of that being taken up by the very last EVAL (the 256-NIL). I will adjust the build sequence to maybe make this directory standard kernel only.

OK, so the slowness is confirmed even with stdknl. And from some previous comments it sounds like the cvcompute part of the new kernel may help greatly but currently is not actually used.

But is the experimental kernel really this slow when doing computations on numbers? I was worrying that the proof may wrongly run into infinite loop. Usually a proof is only tested with -stdknl it may fail with --expk due to some extra variable renaming during the proof (and then fixable by using some rename1). but in rare case it maybe runs into infinite loop.

[binghe]

OK, it took 20m41s here (MacBook 2019 with Intel CPU), stdknl:

Saved theorem _______ "rho_spt_25_example"
Saved theorem _______ "rho_spt_100_example"
Saved theorem _______ "Keccak_224_NIL"
Saved theorem _______ "Keccak_256_NIL"
Exporting theory "keccak" ... done.
Theory "keccak" took 20m41s to build

[mn200]

Indeed, it's possible that there is a bug due to variables, but I think that's pretty unlikely for a ground computation like these. The standard kernel has efficient beta-reduction built in precisely to support EVAL, so it's not surprising that it should do better. There are some other existing instances that demonstrate this (though not in such an extreme way):

• the Miller-Rabin example (examples/miller/miller/selftest.sml)
• the PEG-parsing of s-expressions example (examples/formal-languages/context-free/selftest.sml)

BTW, I don't know if it was the second EVAL in keccak that was really taking "the bulk of the time": when I just redid it, the first one took quite a while too (within a total elapsed time of 13m31s this time).

[mn200]

@xrchz Can you send me (or add via PR) a paragraph on the fact that we have a new example for the release notes in doc/next-release.md please?