Introduce plumbing traits rather than block-only algorithms

[chrysn]

From discussions around #16, it became apparent that the interface proposed isn't quite practical for the parties involved -- the software implementation feared having to go through too much runtime dispatch when it's clear at build time that (eg.) the block collection and padding code is specific to the SHA2 accelerator anyway, and the hardware implementations had constraints that that API couldn't express (eg. the weird 68-byte first block of some STM32s).

This is a 2nd go that aims to be easier.

There's some refactoring to be done here and there, including on the traits (like, where should there be witness types? and: should we really have all traits in one bundle, or have a plumbing::get_sha2() associated function that returns something fallible (a bit like Option<&mut self)>) but using witnesses for positive and negative outcomes to make it dead-code-eliminatable), but that's just Rust API and optimization and shouldn't affect whether or not the API works out for linking hardware and formally verified software.

[jschneider-bensch]

I think this looks good! Thanks for continuously updating the demo implementation as well, that really helps to get an idea of how the traits would be used.

I left some comments on docs.

[WilliamTakeshi]

Sorry for taking so long to review it. I was a bit busy last week.

It looks good to me! I think we can merge and them we can start implement some examples for a couple boards to see how it feels!