sketch Sha256 example end-to-end theorem

[samuelgruetter]

Here's a sketch for an end-to-end theorem about a simple SHA256 program that reads a message from the byte array at input_addr, computes its digest using the bedrock2 driver and Cava Hmac module, and stores the digest into the byte array at digest_addr.
It still contains some admits/TODOs related to bitfiddling and initial states, as well as a bigger TODO indicating that the Cava SHA256 module needs to be integrated as soon as it's ready, but the general structure is there.

For the moment, I made a new directory silveroak-opentitan/Sha256End2End/, and did not yet put it on CI, because it depends on investigations/cava2/, which is not on CI either, and it requires that the directories silveroak-opentitan/hmac/Spec/ and firmware/Hmac are built before this one, but we have not yet discussed how to reflect this dependency on CI.

[jadephilipoom]

Great to have this in place! As for CI, I think we should figure out the configuration sooner rather than later; the cava2 stuff should really be checked as well at this point.