sourcedennis/arancini-proofs repository overview

⁠arancini-proofs

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

See also: sourcedennis/arancini-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 --rm sourcedennis/arancini-proofs:latest agda src/Main.agda --safe

⁠Rendering the proofs

To generate HTML-rendered Agda, run:

docker run --rm -v "$PWD/html:/home/proof/arancini-proofs/html" sourcedennis/arancini-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.