Mainly fix some documentation and remove any Admitted theorems, even though these were in parts of the compiler that were never used.

Main release for OOPSLA'21 paper.

• Add better documentation on how to run Vericert.
• Add Dockerfile with instructions on how to get figures of the paper.

Features

• Added memory inferrence support and proof.

Add a stable release with all proofs completed.

Vericert 1.0.1

Release a new minor version fixing all proofs and fixing scripts to generate the badges.

First release of a fully verified version of Vericert with support for the translation of many C constructs to Verilog.

Feature Support

• Most int instructions and operators.
• Non-recursive function calls.
• Local arrays, structs and unions of type int.
• Pointer arithmetic with int.

This is the first release with working HLS but without any proofs associated with it.