sourcedennis/lasagne-proofs repository overview

⁠lasagne-proofs

Architecture mapping proofs written in Agda for the paper "Lasagne: A Static Binary Translator for Weak Memory Model Architectures"

See also: https://github.com/sourcedennis/lasagne-proofs⁠

This Docker image contains:

• The proofs
• Agda
• Agda's standard library
• Dodo library (https://github.com/sourcedennis/agda-dodo⁠)

⁠Running the proofs

To execute the proofs, run:

docker run -it --rm sourcedennis/lasagne-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/lasagne-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.