diff options
Diffstat (limited to '')
| -rw-r--r-- | README.md | 33 |
1 files changed, 18 insertions, 15 deletions
@@ -12,16 +12,19 @@ Wall in Pompei, digital image from Michael Lahanis. # Aeneas Aeneas is a compiler from LLBC, a language inspired by Rust's MIR, to pure lambda calculus. -It is meant to be used on the output produced by [Charon](https://github.com/Kachoc/charon), -which compiles Rust programs to LLBC, to allow the verification of Rust propgrams in +It is intended to be used in combination with [Charon](https://github.com/Kachoc/charon), +which compiles Rust programs to LLBC, to allow the verification of Rust programs in proof assistants. 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, HOL4 or LEAN. +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 to build the project. -- `fstar`: F\* files providing basic definitions and notations for the code - generated for F\*. +- `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 @@ -43,22 +46,22 @@ 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 +- **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 +- **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<&T>`), - and later address it for functions (i.e., allow `f<&T>` - we consider this to + 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. We might allow nested borrows - while forbiding what we call "borrow overwrites" (see the paper) as a first - step towards supporting this feature. -- no interior mutability: long-term effort. Interior mutability introduces +- **no nested borrows in function signatures**. See the paper for a detailed + discussion. We might allow nested borrows while forbiding what we call + "borrow overwrites" (see the paper) as a first step towards supporting this feature. +- **no interior mutability**: long-term effort. Interior mutability introduces true aliasing: we will probably have to combine our pure lambda calculus with separation logic to address this. Note that interior mutability is mostly anecdotical in sequential execution, but necessary for concurrent execution (it is exploited by the synchronisation primitives). -- no concurrent execution: long-term effort. We plan to address coarse-grained +- **no concurrent execution**: long-term effort. We plan to address coarse-grained parallelism as a long-term goal. |