Interesting, thanks for pointing that out.

This code is such a good example of the potential value of formal verification tools for crypto primitives.