# FreeRTOS VeriFast proofs

This directory contains automated functional correctness proofs of the FreeRTOS
kernel queue data structure. These properties are proven with the
[VeriFast](https://github.com/verifast/verifast) verifier.

## Proof directory structure

We split proofs by data structure into separate proof directories. Each file
within a proof directory is a proof of one or more related API functions. A
proof is the source code of the FreeRTOS implementation with VeriFast
annotations (denoted by special comments `/*@ ... @*/`). A set of common
predicates, functions and lemmas used by all proofs is maintained in the
`include/proof` directory.

  - `queue`: proofs for the FreeRTOS queue data structure

The following figure gives the callgraph of the queue proofs. Green=Proven
functions, Blue=Functions modeled by lock invariants (underlying implementation
assumed to provide these atomicity guarantees), Grey=Assumed stubs.

![Queue proof callgraph](docs/callgraph.png?raw=true "Queue proofs")

## Prerequisites

Proof checking needs VeriFast and proof regression further needs make and perl.

We recommend installing VeriFast from the nightly builds on the [VeriFast
GitHub page](https://github.com/verifast/verifast). After unpacking the build
tarball, the `verifast` and `vfide` binaries will be in the directory
`verifast-COMMIT/bin/` where `COMMIT` is the Git commit of the VeriFast build.

Note that for CI we use [VeriFast 19.12](https://github.com/verifast/verifast/releases).

## Proof checking a single proof in the VeriFast IDE

To load a proof in the `vfide` VeriFast IDE:

```
$ /path/to/vfide -I include queue/xQueueGenericSend.c
```

Then click `Verify` and `Verify Program` (or press F5). Note that the following
proofs require arithmetic overflow checking to be turned off (click `Verify`
and uncheck `Check arithmetic overflow`).

  - `queue/prvCopyDataToQueue.c`
  - `queue/xQueueGenericSendFromISR.c`
  - `queue/xQueueReceiveFromISR.c`

A successful proof results in the top banner turning green with a statement
similar to: `0 errors found (328 statements verified)`.

## Proof checking a single proof at the command-line

The following is an example of checking a proof using the `verifast`
command-line tool. Turn off arithmetic overflow checking where necessary with
the flag `-disable_overflow_check`.

```
$ /path/to/verifast -I include -c queue/xQueueGenericSend.c
```

A successful proof results in output similar to:

```
queue/xQueueGenericSend.c
0 errors found (328 statements verified)
```

## Running proof regression

The following will check all proofs in the repo along with a statement coverage
regression.

```
$ VERIFAST=/path/to/verifast make
```

If you have made changes to the proofs so the statement coverage no longer
matches then you can temporarily turn off coverage checking:

```
$ VERIFAST=/path/to/verifast NO_COVERAGE=1 make
```

## Annotation burden

VeriFast can emit statistics about the number of source code lines and
annotations. These range from .3-2x annotations per line of source code.

```
$ VERIFAST=/path/to/verifast ./scripts/annotation_overhead.sh
```

## Reading a VeriFast proof

VeriFast is a modular deductive verifier using separation logic. A quick
introduction is given by [Jacobs and
Piessens](https://people.cs.kuleuven.be/~bart.jacobs/verifast/verifast.pdf).
In particular, Section 1 Introduction, gives a high-level overview of the proof
technique, which uses forward symbolic execution over a symbolic heap.

Learning how to use VeriFast will help you read and understand the proofs. 
The VeriFast
[tutorial](https://people.cs.kuleuven.be/~bart.jacobs/verifast/tutorial.pdf) is
a good guide. You will need to understand:

  - Sec 4. Functions and Contracts
  - Sec 5. Patterns
  - Sec 6. Predicates
  - Sec 7. Recursive Predicates
  - Sec 8. Loops
  - Sec 9. Inductive Datatypes
  - Sec 10. Inductive Datatypes
  - Sec 11. Lemmas

## Contributors

We acknowledge and thank the following contributors, listed alphabetically:

  - Bart Jacobs, KU Leuven, https://people.cs.kuleuven.be/~bart.jacobs/