<!--
     Copyright 2018, Data61, CSIRO (ABN 41 687 119 230)

     SPDX-License-Identifier: CC-BY-SA-4.0
-->

This is a test suite for running the generated capDL refinement proofs.
These are Isabelle proof scripts, to prove that the generated capDL
respects the isolation properties expected from its CAmkES system
specification.

Currently, the verification only supports apps that use the basic
CAmkES features and connectors.
We plan to extend verification support to more complex CAmkES
assemblies in the future (eventually including a CAmkES VMM).
Also note that only the AARCH32 platform is supported.

When building a CAmkES app, enable proof generation with the
`CAmkESCapDLVerification` option. The proof scripts will be
generated in `projects/camkes` in your build directory. This also
requires `CAmkESCapDLStaticAlloc` to be enabled.

# Tests
The top-level test script is `./run_tests`.

The tests expect to run as part of a
[camkes-manifest](https://github.com/seL4/camkes-manifest) checkout.
In the camkes-manifest repo, do

```
repo sync -m l4v-master.xml
```

This will clone the Isabelle theorem prover and the L4.verified
infrastructure into `projects/l4v`.

Then run the `run_tests` script that is in this directory.