Abstract the sponge construction used in SHA3

[marsella]

The SHA3 spec describes a generic sponge construction, which produces arbitrary-length output when given three components: a function on fixed-length strings, a rate parameter, and a padding rule. As of #137, the Cryptol implementation of SHA3 does not implement a generic sponge construction; it inlines the three components right into the generic algorithm.

It would be better to have a module or a submodule that defines the sponge construction in therms of the three components, and then to instantiate it with the Keccak-specific components. This would more closely match the spec and it would also give us a nice reusable component in case we want to implement, say, Poseidon someday.

• Separate the sponge construction from the Keccak-specific elements in keccak.cry. Might have to fiddle around with submodule vs entirely separate module.
• Update Keccak to instantiate the sponge construction.
• Separate the documentation on the Keccak function from the sponge stuff and update to make it clear how the parts relate and how sponge is reusable.