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, which compiles Rust programs to an intermediate representation called LLBC. It currently has a backend for the F* theorem prover, and we intend to add backends for other provers such as Coq, HOL4 or LEAN.

Project Structure

• src: the OCaml sources. Note that we rely on 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, and install OPAM on the way (same instructions).

The dependencies can then be installed with the following command:

opam install ppx_deriving visitors easy_logging zarith yojson core_unix

When choosing the OCaml compiler version: we compiled Aeneas with version 4.12.1, but any recent version should work.

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

Usage

The simplest way to run Aeneas is to execute dune exec -- src/main.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.