Unknown author, Iapyx removing arrowhead from Aeneas [Fresco].
Wall in Pompei, digital image from Michael Lahanis.
Source
# 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/Kachoc/charon), which compiles Rust programs to an intermediate
representation called LLBC. It currently has backends for the [F\*](https://www.fstar-lang.org)
theorem prover and the [Coq](https://coq.inria.fr/) proof assistant, and we intend to add
backends for other provers such as [HOL4](https://hol-theorem-prover.org/) or [LEAN](https://leanprover.github.io/).
## Project Structure
- `src`: the OCaml sources. Note that we rely on [Dune](https://github.com/ocaml/dune)
to build the project.
- `fstar`: F\* files providing basic definitions and notations for the
generated code (basic definitions for arithmetic types and operations,
collections like vectors, etc.).
- `tests`: files generated by applying Aeneas on some of the test files of Charon,
completed with hand-written files (proof scripts, mostly).
- `rust-tests`: miscelleanous files, to test the semantics of Rust or generate
code in a one-shot manner (mostly used for the arithmetic definitions, for
instance to generate `MIN` and `MAX` constants for all the integer types
supported by Rust).
## 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:
`ln -s PATH_TO_CHARON_REPO/charon-ml charon`
**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.
We have the following limitations, that we plan to address one by one:
- **no loops**: ongoing work. We are currently working on a "join" operation on
environments to address this issue.
- **no functions pointers/closures/traits**: ongoing work.
- **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.
- **no interior mutability**: long-term effort. Interior mutability introduces
true aliasing: we will probably have to use a low-level memory model to address
this issue.
Note that interior mutability is truely necessary for concurrent execution (it
is exploited to implement the synchronisation primitives).
- **no concurrent execution**: long-term effort. We plan to address coarse-grained
parallelism as a long-term goal.
## 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)).