"x /^ y" is x/y rounded up, i.e. the least n such that x <= y*n.
"x %^ y" is the least k such that x+k is a multiple of y.
For comparison,
"x / y" is x/y rounded down, i.e. the greatest n such that x >= y*n.
"x % y" is the least k such that x-k is a multiple of y.
The new syntax is much more suggestive of the relation to "/" and "%".
Cryptol could not prove that subtracting `65 + padding` from `512 * chunks`
in the constraint `msgLen == 512 * chunks - (65 + padding)` was well
defined, and rejected the function. This constraint was redundant, so
removing it allowed the function to typecheck.
