Oracle-FormalMethods

The formalization files are inside the folder oracle-formalization and comprise of:

• Hexadecimal.v
• Datatypes.v
• Functions.v
• Theorems.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.