diff options
Diffstat (limited to '')
| -rw-r--r-- | README.md | 41 |
1 files changed, 21 insertions, 20 deletions
@@ -13,24 +13,18 @@ Wall in Pompei, digital image from Michael Lahanis. 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/). +[Charon](https://github.com/AeneasVerif/charon), which compiles Rust programs to an intermediate +representation called LLBC. It currently has backends for [F\*](https://www.fstar-lang.org), +[Coq](https://coq.inria.fr/), [HOL4](https://hol-theorem-prover.org/) and [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.). +- `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). -- `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 @@ -83,27 +77,34 @@ to display a detailed documentation. ## Targeted Subset And Current Limitations -We target **safe** Rust. +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: -- **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. +- **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. -- **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). +- **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`). + ## Formalization The translation has been formalized and published at ICFP2022: [Aeneas: Rust |