The formalization files are inside the folder oracle-formalization
and comprise of:
Hexadecimal.vDatatypes.vFunctions.vTheorems.v
To compile the formalization, type make at the top level directory.
To run any of the formalization files, open the file with your preferred Coq IDE (emacs/ProofGeneral, CoqIDE, vsCoq, etc) after compilation.
You can clean the compiled files by typing make clean at the top
level directory.