Holy shit these claims are wild!
It's not just a percent more performance here and there, the graphs look more like 50% more throughput on the same hardware (depending on the cpu architecture).
My immediate fear was that they optimized away the security features like absence of timing side channels, but they say they still have those.
They also claim to have formal proof of correctness, which is even more amazing, because they are not doing it on a symbolic level but on a machine instruction level. Apparently they tought their reasoning system the semantics of all the CPU instructions used in the assembler implementation.
I'll still wait what djb has to say about this, but it looks freaking amazing to me.
My immediate fear was that they optimized away the security features like absence of timing side channels, but they say they still have those.
They also claim to have formal proof of correctness, which is even more amazing, because they are not doing it on a symbolic level but on a machine instruction level. Apparently they tought their reasoning system the semantics of all the CPU instructions used in the assembler implementation.
I'll still wait what djb has to say about this, but it looks freaking amazing to me.