Simple coq lemmas

[scuellar]

This PR adds a handful of CN examples with CN lemmas that can be exported into Coq. There are several limitations to these exports, notably:

1. No recursive definitions
2. No ownership
3. Unsupported functions (such as bitwise operators). Although this is really a limitation of the language, not the Coq export.
4. All bounded integers (e.g. int), are exported as Coq Z, with a handful of bounds. That conversion is not correct.

---

To export lemmas in the new directory use

cn --lemmata=build/theories/ExportedLemmas.v example-file.c

which will create the lemmas in the build/theories/ directory next to the other required files. See src/example-archive/coq-lemmas/README.md for details.

[scuellar]

@septract I've extended the check.sh script to also extract and build coq lemmas. For this, I've added a new (optional) folder in the examples with the following organization:

• <source>/coq/* - examples that CN verifies without error and have lemmas that should be extracted. According to the following rules
  • <source>/coq/working - Examples where Coq lemmas can be extracted and the Coq project can be built.
  • <source>/coq/broken-build - Examples where Coq lemmas can be extracted, but the Coq build process fails.
  • <source>/coq/broken-export - Examples where Coq extraction fails. These should still be verifiable with CN.

The new script extracts lemmas for any example in these directories and checks for the expected result. If proofs are present, they are also built but we do not check if the proofs exists. This might be hard to do.

I've completely changed the README to follow your suggestions, describing the batch build and single-example build.

---

More details on the build process

For each example, we need a build folder to put the extracted lemmas, the proofs, the cn library lemmas, the _CoqProject, the (auto generated) Makefile and all the generated *.vo files when the coq files are properly built.

For convenience I've created a prototype build folder at cn-tutorial/src/example-archive/coq-biuld. This directory contains the _CoqProject and the theories/CN_Lib.v file with cn lemmas. I assume this file will grow in the future so avoiding repetition is key.

For each example, the build script uses rsync copy/update the build folder. Then the script (1) generates the Coq lemmas, (2) creates a Makefile for the project, and (3) builds the project, verifying the Coq files.

If a file with proofs is present it will be built and verified, but we do not check for this. It would be easy to check for the presence of the theories/Proofs.v file, but checking that it proofs the right thing would be tricky.

[septract]

Merged without enabling CI, as this requires a change to the cerberus CI script as well.

Here's a PR that would enable Coq examples in CI: #40