search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
621 stars 140 forks source link

Get Keccak hash function to evaluate fast using cv compute #1234

Closed xrchz closed 4 months ago

binghe commented 4 months ago

Hi, I wonder how fast is it now, in both std and expk kernels? (it was half a hour in std and 10 hours in expk)

myreen commented 4 months ago

On my desktop machine, the entire script now takes just under one minute to build using the stdknl. I suspect the timing will be similar for expk, but haven't tried expk.

myreen commented 4 months ago

I've now tested it with expk. With expk, keccakTheory builds in exactly one minute on my now quite old desktop computer.

myreen commented 4 months ago

On an Apple M2 Max MacBook Pro it runs in 30 second, i.e., twice as fast!

Note that all of my measurements here are for building the entire theory rather than just doing the evaluation at the end of the theory. The evaluations are quick. On the MacBook, each evaluation takes a second.