translate keccak permutation into CakeML

several of the functions have unproveable-looking side-conditions, e.g.
because of under-specification (partiality).