This artifact provides the supplementary Coq development for the Making Weak Memory Models Fair paper from OOPSLA'21. The easiest way to check proofs is to use the prepared virtual machine. 1. Install VirtualBox (we tested the process with version 6.1) with Oracle VM VirtualBox Extension pack. 2. Open VirtualBox and navigate to File/Import Appliance. Provide the path to the artifact.ova file and follow instructions to create a VM. 3. Run the newly created VM. If a "RawFile#0 failed to create the raw output file ..." error occurs, try disabling serial ports in VirtualBox (right click on VM -> Settings -> Serial Ports -> uncheck "Enable Serial Port" boxes). See the discussion of the related problem. 4. Login with username and password "vagrant". 5. Navigate to /home/vagrant/artifact_compiled in a terminal and run make -j 4. Since proofs are pre-compiled, it should terminate in a second. You may also run make clean; make -j 4 to recompile proofs from scratch (adjust the -j parameter according to the number of available cores). 6. Run grep -HRi admit to ensure there are no incomplete proofs. 7. Check that Coq formalization matches the paper's claims (details are in README.md). 8. The VM includes configured Emacs w/ Proof General and Vim w/ Coqtail so you can edit proofs interactively. The detailed description of the artifact and instructions for environment reproduction are specified in README.md.

This research was supported in part by the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement no. 851811 and 101003349). Lahav was also supported by the Israel Science Foundation (grant number 1566/18) and by the Alon Young Faculty Fellowship.