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
|
<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/Kachoc/charon), which compiles Rust programs to an intermediate
representation called LLBC. It currently has a backend for the [F\*](https://www.fstar-lang.org)
theorem prover, and we intend to add backends for other provers such as
[Coq](https://coq.inria.fr/), [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
```
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.
## Documentation
If you run `make`, you will generate a documentation accessible from [`doc.html`](./doc.html).
## 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.
## 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)).
|
