Combine Uart and SHA256 proofs

[samuelgruetter]

Compared to the lightbulb's end-to-end theorem, ours currently does not involve any I/O with the external world, but it might actually be quite easy to add that.

More concretely, I'm thinking of the following steps:

• Replace the init/update/finish calls to SHA256 in sigverify.c by our verified b2_sha256
• Add a call to uart_write to our verified b2_sha256 which logs the computed digest to UART
• Check whether the whole thing still runs on an FPGA if we replace that code with our verified code
• Update the RISC-V machine models used in the end-to-end proofs to not only include "internal" MMIO (ie to the Cava SHA256 device), but also "external" MMIO (ie not being consumed by another verified device, but going to the "external world"), and adapt the end-to-end theorem to state that the event trace includes Uart messages that contain the hash that was logged.

Once that works, we could also consider verifying sigverify_rsa_verify (while assuming correctness of the crypto-related functions it calls) and log a "signature ok"/"bad signature" string instead of just logging the hash.

[jadephilipoom]

This seems like a really good idea, especially for communication purposes; interaction is useful for papers and demos. We could also potentially (not as an immediate goal, since I assume it would involve nontrivial extra work -- would it?) make an end-to-end proof that incorporates the UART proofs as well, so that we have a proof that involves two peripheral devices interacting with each other.

[samuelgruetter]

make an end-to-end proof that incorporates the UART proofs as well

I think we should give that a try in the next few months! (even though cava_hmac_satisfies_state_machine has higher priority)