summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--README.md41
1 files changed, 21 insertions, 20 deletions
diff --git a/README.md b/README.md
index 3acba834..31dc74f4 100644
--- a/README.md
+++ b/README.md
@@ -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