OwenConoly
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](https://github.com/mit-plv/riscv-semantics/tree/master) instead. But this PR should be...
This PR will add leakage traces to the source and intermediate semantics, augment the compiler-correctness statement and proof to talk about leakage traces, and add some examples involving leakage traces.
An extensionality hypothesis of the `Fix_eq` lemma is unnecessarily strong, so I have weakened it here. I've had some mild inconvenience with proving fixpoint equations, which would've been alleviated by...
I am not actually requesting that this be pulled, but maybe it is interesting. This branch's version of MetricLeakageSemantics uses a version of omnisemantics that allows proving things about nonterminating...
I spent a while looking at the proof of `withInterference_parallel` (in the ModelChecking file) without being able to understand it, so I tried to write a simpler proof. Obviously my...