Arm8 weak memory model

This repository contains the Arm8 memory model with support for mixed-size accesses.

Prerequisites:

• Rocq version 8.20.1 (https://rocq-prover.org/)

Compilation instructions:

git submodule init
git submodule update
cd hahn; make; cd ..
cd arm-model; make

~