sourcedennis/risotto-proofs repository overview

⁠risotto-proofs

Architecture mapping proofs written in Agda for the paper "Risotto: A Dynamic Binary Translator for Weak Memory Architectures"

See also: binary-translation/risotto-proofs⁠

This Docker image contains:

• The proofs
• Agda
• Agda's standard library
• Dodo library (sourcedennis/agda-dodo⁠)

⁠Running the proofs

To execute the proofs, run:

docker run -it --rm sourcedennis/risotto-proofs:latest agda src/Main.agda --safe

⁠Rendering the proofs

To generate HTML-rendered Agda, run:

docker run -it --rm -v "$PWD/html:/proofs/html" sourcedennis/risotto-proofs:latest agda --html --html-dir=html src/Main.agda

Note that this creates a local html/ directory. You can open html/Main.html in any browser.