Unknown author, Iapyx removing arrowhead from Aeneas [Fresco]. Wall in Pompei, digital image from Michael Lahanis. Source

Aeneas [Ae-ne-as]

Aeneas (pronunced [Ae-ne-as]) 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 backends for F*, Coq, HOL4 and LEAN.

If you want to contribute or ask questions, we strongly encourage you to join the Zulip.

Project Structure

src: the OCaml sources. Note that we rely on 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, 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 project. The simplest way is to clone Charon, then go to 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):

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 test and make verify to run the tests, and check the generated files. As make test will run tests which use the Charon tests, you will need to regenerate the .llbc files. You have the following options:

run make test in the Charon repository
run make test in the Aeneas repository

Documentation

If you run make, you will generate a documentation accessible from doc.html.

Usage

The Aeneas binary is in bin; you can run: ./bin/aeneas -backend {fstar|coq|lean|hol4} [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.

Additional Steps for Lean Backend

Files generated by the Lean backend import the Base package from Aeneas. To use those files in Lean, create a new Lean package using lake new, overwrite the lean-toolchain with the one inside ./backends/lean, and add base as a dependency in the lakefile.lean:

require base from "PATH_TO_AENEAS_REPO/backends/lean"

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.

Formalization

The translation has been formalized and published at ICFP2022: Aeneas: Rust verification by functional translation (long version).

RaitoBezarius/aeneas