summaryrefslogtreecommitdiff
path: root/README.md
blob: 641004109bbe6bc2326f44f56babb42b4d9b2ce4 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
<p><div style="text-align: center">
<img src="static/Aeneas.jpg"
     alt="Iapyx removing arrowhead from Aeneas" title="Iapyx removing arrowhead from Aeneas"
     style=""/>
<figcaption>
Unknown author, <i>Iapyx removing arrowhead from Aeneas</i> [Fresco].
Wall in Pompei, digital image from Michael Lahanis.
<a href="https://commons.wikimedia.org/w/index.php?curid=1357010">Source</a>
</figcaption>
</div></p>

# Aeneas

Aeneas is a verification toolchain for Rust programs.  It relies on a translation from Rusts's MIR
internal language to a pure lamdba calculus.  It is intended to be used in combination with
[Charon](https://github.com/AeneasVerif/charon), which compiles Rust programs to an intermediate
representation called LLBC. It currently has backends for [F\*](https://www.fstar-lang.org),
[Coq](https://coq.inria.fr/), [HOL4](https://hol-theorem-prover.org/) and [LEAN](https://leanprover.github.io/).

If you want to contribute or ask questions, we strongly encourage you to join the [Zulip](https://aeneas-verif.zulipchat.com/).

## Project Structure

- `src`: the OCaml sources. Note that we rely on [Dune](https://github.com/ocaml/dune)
  to build the project.
- `backends`: standard libraries for the existing backends (definitions for
   arithmetic operations, for standard collections like vectors, theorems, tactics, etc.)
- `tests`: files generated by applying Aeneas on some of the test files of Charon,
  completed with hand-written files (proof scripts, mostly).

## Installation & Build

You need to install OCaml, together with some packages.

We suggest you to follow those [instructions](https://ocaml.org/docs/install.html),
and install OPAM on the way (same instructions).

We use **OCaml 4.13.1**: `opam switch create 4.13.1+options`

The dependencies can then be installed with the following command:

```
opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc \
  unionFind ocamlgraph
```

Moreover, Aeneas requires the Charon ML library, defined in the
[Charon](https://github.com/AeneasVerif/charon) project.
The simplest way is to clone Charon, then go to [`compiler`](./compiler) and
create a symbolic link to the Charon library:
`cd AENEAS_REPO/compiler && ln -s PATH_TO_CHARON_REPO/charon-ml charon`
(the symbolic link should be placed inside the `aeneas/compiler/` folder).

**Remark:** if you want to test if the symbolic link is valid, copy-paste the
following script in your terminal (from the `compiler` directory):
```bash
if [ -e charon ]; then echo "valid"; else echo "invalid"; fi
```

Finally, building the project simply requires to run `make` in the top
directory.

You can also use `make tests` and `make verify` to run the tests, and check
the generated files. As `make tests` will run tests which use the Charon tests,
you will need to regenerate the `.llbc` files. You have the following options:
- run `make tests` in the Charon repository
- run `REGEN_LLBC=1 make tests` in the Aeneas repository

## Documentation

If you run `make`, you will generate a documentation accessible from [`doc.html`](./doc.html).

## Usage

The Aeneas binary is in `bin`; you can run: `./bin/aeneas.exe [OPTIONS] LLBC_FILE`,
where `LLBC_FILE` is an .llbc file generated by Charon.

Aeneas provides a lot of flags and options to tweak its behaviour: you can use `--help`
to display a detailed documentation.

## Targeted Subset And Current Limitations

We target **safe** Rust. This means we have no support for unsafe Rust, though we plan to
design a mechanism to allow using Aeneas in combination with tools targeting unsafe Rust.

We have the following limitations, that we plan to address one by one:

- **loops**: no nested loops for now. We are working on lifting this limitation.
- **no functions pointers/closures/traits**: ongoing work. We are actively working on this
  and plan to have support soon.
- **limited type parametricity**: it is not possible for now to instantiate a type
  parameter with a type containing a borrow. This is mostly an engineering
  issue. We intend to quickly address the issue for types (i.e., allow `Option<&mut T>`),
  and later address it for functions (i.e., allow `f<&mut T>` - we consider this to
  be less urgent).
- **no nested borrows in function signatures**: ongoing work.
- **interior mutability**: ongoing work. We are thinking of modeling the effects of
  interior mutability by using ghost states.
- **no concurrent execution**: long-term effort. We plan to address coarse-grained
  parallelism as a long-term goal.

## Backend Support

We currently support F\*, Coq, HOL4 and Lean. We would be interested in having an Isabelle
backend. Our most mature backends are Lean and HOL4, for which we have in particular
support for partial functions and extrinsic proofs of termination (see
`./backends/lean/Base/Diverge/Elab.lean` and `./backends/hol4/divDefLib.sig` for instance)
and tactics specialized for monadic programs (see
`./backends/lean/Base/Progress/Progress.lean` and `./backends/hol4/primitivesLib.sml`).

A tutorial for the Lean backend is available [here](./tests/lean/Tutorial.lean).

## Formalization

The translation has been formalized and published at ICFP2022: [Aeneas: Rust
verification by functional
translation](https://dl.acm.org/doi/abs/10.1145/3547647)
([long version](https://arxiv.org/abs/2206.07185)).