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.

[septract]

Small changes:

• I think this needs more explanation of how to run the examples
• I assume you have proofs of some of these examples. Can you check these in? eg. you could call this trivial-001.v and keep them alongside the example files
• Some small stuff, eg. issues with the path in the makefile

Bigger ask: Ideally, I'd like a script that we can add to CI that checks this feature is working properly. This could be:

• Run the export function and check it still works (easy, we just need to run CN on all the individual files)
• Check that Coq can parse the result, even if the proof isn't successful (a little more fiddly)
• Make the script copy a reference proof of each lemma in place and check it using coq (great, but depends on whether we actually have such proofs

[septract]

Typo: "Prove"

[septract]

Incorrect path

[septract]

Inconsistent line wrapping wrt above

[septract]

Remove WIP, as they don't seem to be included in this PR?

[septract]

This explanation isn't enough for me to know what to do. In which file does Lemma_Spec go? As I said above, it would be good to have an idiot-proof process for replicating the proofs

[septract]

I thought recursive definitions weren't working?

[scuellar]

Correct. These are examples of recursive definitions we want to work. The provided recursive examples pass the CN verification but fail to export.

I'll add clarification.

[septract]

I think this file should begin with instructions for running all the examples in batch, or individually. something like:

To build and verify the example trivial-0001.c do the following:

• Run CN as follows ...
• Copy the sample proof to ...
• Run the make file as follows

Something extremely idiot-proof

[septract]

I'm not sure what the purpose of this Makefile is - do I call it during the proof process?

[septract]

Isn't this file going to be auto-generated by CN - why include a skeleton?

[septract]

Needs some brief description what coq tools need to be installed to run the examples

[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