samuelgruetter
commented
4 months ago 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.
One could say that leakage is something you only need for reasoning, not in simulation, and that therefore it's fine to write it directly in Coq. On the other hand, if you believe that other use cases could benefit from your definitions as well, you could also write them in Haskell, but then it would be good to follow some official spec as closely as possible.
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.
I'm not sure if the 'associate leakage with basic operations' approach would work: There is currently no basic operation in the typeclass to record branching, and adding one that gets called in ExecuteI seems too invasive because most users of that file are not interested in leakage.
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.
Leaking fetch addresses would make sense, imho.
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.
Would be nice indeed. (but also, don't aim for a would-be-nice that you can't finish before leaving for your next career step -- I don't know your schedule but I'd rather have your current code merged than halfway improved towards something better but unmerged)
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.
I'd be fine with either merging almost-as-is or with doing it in Haskell. If you decide not do write Haskell, I'd request the following changes to the current code:
- Move the changes of
Decode.vinto a separate file, because that's a file automatically translated with hs-to-coq - Cleanup, including: I'm not sure whether the additions to
MetricMinimalMMIO.vare actually needed, andMetricMinimalNoMul.v/MinimalNoMul.vwere deleted (moved to softmul) at some point, so you shouldn't add them back, noPrint/Searchetc commands
OwenConoly
andres-erbsen
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.