The post condition on Crypto.Phelix.H isn't very readable, this should be improved. It would be nice to have it expressed in a form that side-by-side comparison with the algorithm specification would be possible.