Cerisier: A Program Logic for Attestation in a Capability Machine (Artifact)

This is the artifact accompanying the article "Cerisier: A Program Logic for Attestation in a Capability Machine" at PLDI'26. The artifact contains the Rocq proofs accompanying the paper, built using the Iris framework. We provide The Rocq sources themselves under cerisier.tar.gz; A virtual machine cerisier.ova with a prebuilt version of the development. The VM already has Emacs and Proof General installed to explore the proofs. The project is available in the directory ~/Desktop/cerisier-artifact-pldi26 in the VM. There is no password required. Follow the instructions in the README.md, available in cerisier.tar.gz. Don't hesitate to contact us if you have any questions!