New  Third phase of performance analysis, improvement, and porting the library to GNAT and SPARK Community 2021 is written up here.

Second phase of performance analysis is now written up here.

I’m pleased to say that I’ve finished the first phase of performance analysis and tuning of the SPARKNaCl library. This has been something of a marathon, and touched on all sorts of interesting topics with SPARK, proof, language design, compiler internals, and the details of the RISC-V ISA and its implementation.

The write-up is on AdaCore’s blog as before. This is the most nerdy/technical thing I’ve worked on and written for ages, but please have a look. TL;DR version: formal is fast!

You can see all the updates and tagged snapshots of the code as I worked on it on SPARKNaCl’s GitHub Repo.

An update for SPARKNaCl in the ALIRE package manager will follow shortly.