Leakage Traces

[OwenConoly]

Adds leakage traces to the semantics.

I'm unsure whether the leakage trace semantics actually belong in this repository; maybe they should go in riscv-semantics instead. But this PR should be a fine place to discuss whether these changes belong here.

Another basic question about this PR, which I don't know the answer to: should we associate leakage with assembly instructions (as it currently is in this branch), or should we associate leakage with basic operations that the machine does? To elaborate: currently, I've modified the definition of a cycle so that, before executing each instruction, we first leak (the appropriate function of) the instruction. Alternatively, taking the 'associate leakage with basic operations' approach, we could just say that the appropriate things are leaked while the instruction is being executed. For example, we would modify the definition of the loadByte function (wherever it's defined) so that it leaks whatever address it loads.

A downside of the leak-instructions approach is that the instruction fetch locations (program counter values) aren't explicitly leaked. (Arguably this doesn't matter at all, since we do leak branches.) But we could further modify the definition of a cycle so that they are leaked.

I think Andres mentioned to me that there exists an official RISC-V specification saying what should be leaked by different instructions? If we stick with the leak-instructions approach, then I expect we could have a line-to-line-ish correspondence between our leakage spec in Haskell/Coq and the spec in English. This would be nice.

The code in this branch is a bit of a mess, and the semantics of some instructions (e.g., CSR instructions, which I am not very familiar with) are probably wrong. I figured I'd try to answer questions like "should I rewrite this in Haskell" before taking the time to clean it up.