Comment by ecesena

Yeah, I hear you. Many things are simplified in this crypto code, for example there’s no dynamic allocation. At the same time it’s incredibly difficult to get a realistic model of the hardware instructions because they all have side effects. And it gets incredibly more difficult if you try to prove real world, hand optimized code (vs academic proof of concept code).

With all this said, I think this could be a good inspiration and look forward to seeing advancements!