aeneasverif/aeneas

A verification toolchain for Rust programs

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).

aeneas's Issues

Lean backend: do not use `by intlit` in the generated code

Make the proof that integers are in bound implicit when generating the code (i.e., do not use by intlit).
See: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/instance.20with.20tactic.20autoparam

Iterating over a slice causes a crash in `stdlib.ml`

For the following Rust function:

fn zero_slice(a: &mut [u8]) {
    let mut i: usize = 0;
    let len = a.len();
    while i < len {
        a[i] = 0;
        i = i + 1;
    }
}

Aeneas crashes with an uncaught exception in stdlib.ml:

$ charon
   Compiling array_zero v0.1.0 (/home/ubuntu/examples/aeneas/array_zero)
[ INFO charon_driver::export:106] [gexport]: Generated the file: /home/ubuntu/examples/aeneas/array_zero/array_zero.llbc
    Finished release [optimized] target(s) in 0.17s
$ aeneas -backend lean array_zero.llbc 
[Info ] Imported: array_zero.llbc
Uncaught exception:
  
  (Invalid_argument "option is None")

Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
Called from Aeneas__InterpreterBorrows.end_abstraction_aux in file "InterpreterBorrows.ml", line 967, characters 12-37
Called from Aeneas__InterpreterUtils.get_cf_ctx_no_synth in file "InterpreterUtils.ml", line 26, characters 10-18
Called from Aeneas__InterpreterLoopsFixedPoint.compute_loop_entry_fixed_point.join_ctxs in file "InterpreterLoopsFixedPoint.ml", line 403, characters 21-52
Called from Aeneas__InterpreterLoopsFixedPoint.compute_loop_entry_fixed_point in file "InterpreterLoopsFixedPoint.ml", line 476, characters 11-60
Called from Aeneas__InterpreterLoops.eval_loop_symbolic in file "InterpreterLoops.ml", line 76, characters 4-68
Called from Aeneas__InterpreterLoopsFixedPoint.prepare_ashared_loans in file "InterpreterLoopsFixedPoint.ml", line 306, characters 8-14
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterPaths.end_loans_at_place in file "InterpreterPaths.ml", line 558, characters 4-10
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterStatements.eval_function_call_symbolic_from_inst_sig.cf_call in file "InterpreterStatements.ml", line 1403, characters 15-21
Called from Aeneas__InterpreterPaths.end_loans_at_place in file "InterpreterPaths.ml", line 558, characters 4-10
Called from Aeneas__InterpreterStatements.eval_transparent_function_call_symbolic in file "InterpreterStatements.ml", line 1307, characters 2-161
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterStatements.eval_statement.cf_eval_st.cf_assign in file "InterpreterStatements.ml", line 955, characters 29-70
Called from Aeneas__InterpreterPaths.end_loans_at_place in file "InterpreterPaths.ml", line 558, characters 4-10
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterPaths.end_loans_at_place in file "InterpreterPaths.ml", line 558, characters 4-10
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterStatements.eval_statement.cf_eval_st.cf_assign in file "InterpreterStatements.ml", line 955, characters 29-70
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.expand_symbolic_value_borrow in file "InterpreterExpansion.ml", line 419, characters 17-23
Called from Aeneas__Interpreter.evaluate_function_symbolic in file "Interpreter.ml", line 589, characters 4-71
Called from Aeneas__Translate.translate_function_to_symbolics in file "Translate.ml", line 35, characters 25-77
Called from Aeneas__Translate.translate_function_to_pure in file "Translate.ml", line 55, characters 23-69
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 298, characters 4-127
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 992, characters 4-33
Called from Dune__exe__Main in file "Main.ml", line 279, characters 6-58

Charon version: AeneasVerif/charon@9aedfc3
Aeneas version: eb8bddc

Check that functions are well-formed for extrinsic proofs of termination

Our current encoding of the functions in HOL4, which allows extrinsic proofs of termination, has constraints with regards to the use of higher-order functions. We may have a solution for this, that we will test in Lean, but for the time being it might be good to check that the functions we generate are in the supported subset.

Add support for mutually recursive functions in Lean

Mutually recursive functions are currently not supported in Lean, because the syntax for the termination_by, decreasing_by clauses in case of mutually recursive functions is not obvious. Once this is done (or we fix this by allowing extrinsic proofs of termination in a fashion similar to what we do in HOL4 now) we will need to reactivate the compilation of the betree.

Get rid of the Makefiles

The Makefiles are getting bloated in particular when it comes to the test generation, and are probably not the best way of managing a project like Aeneas today. It would probably better to have scripts or use dune/cargo (if we add a Rust executable) for everything.

Register a theorem for induction over positive integers

This might prove useful:
https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2024-03-28

Improve the formatting of the generated code

The formatting of some code blocks is not always pretty and in particular indentation is sometimes weird (for instance, the indentation of the do ... blocks in Lean). Also, it would probably be better to use the PPrint module.

Incorrect indexing for tuple structs in Lean backend

For the following tuple struct:

pub struct Foo(i32, bool, u8);

impl Foo {
    pub fn new() -> Foo {
        Foo(0, false, 1)
    }

    pub fn get_first(&self) -> i32 {
        self.0
    }

    pub fn get_second(&self) -> bool {
        self.1
    }

    pub fn get_third(&self) -> u8 {
        self.2
    }
}

Aeneas generates the following Lean code:

-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [tuple_index]
import Base
open Primitives

namespace tuple_index

/- [tuple_index::Foo]
   Source: 'src/main.rs', lines 1:0-1:14 -/
def Foo := I32 × Bool × U8

/- [tuple_index::{tuple_index::Foo}::new]:
   Source: 'src/main.rs', lines 4:4-4:23 -/
def Foo.new : Result Foo :=
  Result.ret (0#i32, false, 1#u8)

/- [tuple_index::{tuple_index::Foo}::get_first]:
   Source: 'src/main.rs', lines 8:4-8:34 -/
def Foo.get_first (self : Foo) : Result I32 :=
  Result.ret self.0

/- [tuple_index::{tuple_index::Foo}::get_second]:
   Source: 'src/main.rs', lines 12:4-12:36 -/
def Foo.get_second (self : Foo) : Result Bool :=
  Result.ret self.1

/- [tuple_index::{tuple_index::Foo}::get_third]:
   Source: 'src/main.rs', lines 16:4-16:33 -/
def Foo.get_third (self : Foo) : Result U8 :=
  Result.ret self.2

end tuple_index

The indexing used in get_first, get_second, etc is invalid in Lean, as the Prod type only has Prod.1 and Prod.2 (which are shorthand for Prod.fst and Prod.snd):

https://github.com/leanprover/lean4/blob/815200eaad2a0fe31ef24df9ea37a2f3a054a4a1/src/Init/Prelude.lean#L475

Do not copy paste the `Primitives.{v,fst}` files at code generation time

Remove the sorries from the Lean backend

Some proofs in the Lean backend (Primitives.lean) are unfinished and use sorry

Reorganize the `compiler` folder into subfolders

Move the information about the definitions from the standard library to an external file

For now, the definitions supported by our standard libraries are hardcoded in ExtractBuiltin.ml. This information should be moved to an external file which should be read at runtime.

Improve the pretty-printing of coerced machine integers

If x is a machine integer (e.g., U32), Lean often displays x coerced to Int as x.val instead of ↑x. This can make the proof states quite difficult to parse, even when they are small. For instance, see the difference between this context:

x : U32
h : 2 * x.val + 1 ≤ U32.max
i : U32
_¹ : i.val = x.val + x.val
i' : U32
_ : i'.val = i.val + 1#u32.val

and this context:

x : U32
h : 2 * ↑x + 1 ≤ U32.max
i : U32
_¹ : ↑i = ↑x + ↑x
i' : U32
_ : ↑i' = ↑i + ↑1#u32

Use namespaces and shorten the generated names

Currently, all the definitions generated by Aeneas are prefixed and suffixed to prevent name collisions. This generates very long names, which are cumbersome to work with when writing proofs (for instance, hash_map_new_with_capacity_fwd). It would be good to make those names shorter.

For instance, in backends like Coq and Lean it would be possible to use namespaces (HashMap.new_with_capacity_fwd, for instance), which would allow to use shorter names when possible (new_with_capacity_fwd) and disambiguate when needed. Lean seems especially suited for this, as it is extremely flexible; for instance, it accepts the following definitions, which belong to different namespaces that we declare on the fly (this would be useful for Rust, because groups of mutually recursive definitions can span across different modules):

mutual
def F.f (i : Nat) : Bool :=
  if i = 0 then true else G.f (i - 1)

def G.f (i : Nat) : Bool :=
  if i = 0 then false else F.f (i - 1)
end

Also, it is maybe not really useful to always add a suffix to definitions. In particular, we could omit the fwd, back, etc. suffixes when there is no backward function, or when we filter the forward function. For instance, hash_map_new_with_capacity_fwd would become HashMap.new_with_capacity. Generally speaking, it is safe to be a bit lax with regards to the name collisions: any name collision is detected by Aeneas at compile time: if there is such a collision, it is possible to rename the involved definition to avoid the collision.

In the future, it would also be good to allow the user to annotate the definitions with attributes so as to tweak the generated names.

A struct with a reference causes a crash in SymbolicToPure.ml

Code:

struct Foo<'a> {
    x: &'a i32,
}

fn main() { }

Output:

$ charon
   Compiling ref_in_struct v0.1.0 (/home/ubuntu/examples/aeneas/ref_in_struct)
[ INFO charon_driver::export:106] [gexport]: Generated the file: /home/ubuntu/examples/aeneas/ref_in_struct/ref_in_struct.llbc
    Finished release [optimized] target(s) in 0.15s
$ aeneas -backend lean ref_in_struct.llbc 
[Info ] Imported: ref_in_struct.llbc
Uncaught exception:
  
  "Assert_failure SymbolicToPure.ml:554:2"

Raised at Aeneas__SymbolicToPure.translate_type_decl in file "SymbolicToPure.ml", line 554, characters 2-23
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 277, characters 19-64
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 992, characters 4-33
Called from Dune__exe__Main in file "Main.ml", line 279, characters 6-58

Crash when extracting reference to `Self`

The following code makes Aeneas crash:

pub trait MinimumTraitExample {
    const CONSTANT: u32 = 10;

    fn uses_self() -> u32 {
        Self::CONSTANT
    }
}

Error:

Uncaught exception:
  
  (Failure "Unexpected occurrence of `Self`")

Raised at Aeneas__ExtractTypes.extract_trait_instance_id in file "ExtractTypes.ml", line 664, characters 8-57
Called from Aeneas__ExtractTypes.extract_trait_ref in file "ExtractTypes.ml", line 581, characters 2-68
Called from Aeneas__Extract.extract_App in file "Extract.ml", line 340, characters 10-71
Called from Aeneas__Extract.extract_adt_cons.(fun) in file "Extract.ml", line 532, characters 8-44
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Aeneas__Extract.extract_adt_g_value in file "Extract.ml", line 177, characters 10-170
Called from Aeneas__Extract.extract_adt_cons in file "Extract.ml", line 530, characters 4-174
Called from Aeneas__Extract.extract_fun_decl_gen in file "Extract.ml", line 1546, characters 12-77
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Aeneas__Translate.export_functions_group_scc in file "Translate.ml", line 561, characters 4-42
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Aeneas__Translate.export_functions_group in file "Translate.ml", line 642, characters 7-80
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 768, characters 2-52
Called from Aeneas__Translate.extract_file in file "Translate.ml", line 886, characters 2-36
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1431, characters 5-42
Called from Dune__exe__Main in file "Main.ml", line 277, characters 6-58

Make the bounds for `isize`/`usize` opaque in F*

As of today, all the backends have opaque bounds for isize and usize (because those depend on the architecture) but F*: update this.

Add checks for uniform polymorphisms (HOL4)

HOL4 only supports uniform polymorphism, which is not granted by Rust: it would be good to check this, and at least print a warning if the functions we translate/the generated functions don't fall into the supported subset.

Improve the formatting functions

We should improve the formatting functions (in Print.ml for instance). In particular, we should use the Format or PPrint module instead of directly generating string (the indentations and the breaklines we generate are not pretty).

A crash in SymbolicToPure.ml when a reference to an integer literal is used in a comparison

Code:

fn main() {
    let x = 1;
    let _ = &x == &1;
}

Output:

$ charon
   Compiling ref_comp v0.1.0 (/home/ubuntu/examples/aeneas/ref_comp)
^[[A[ INFO charon_driver::export:106] [gexport]: Generated the file: /home/ubuntu/examples/aeneas/ref_comp/ref_comp.llbc
    Finished release [optimized] target(s) in 0.18s
$ aeneas -backend lean ref_comp.llbc 
[Info ] Imported: ref_comp.llbc
Uncaught exception:
  
  "Assert_failure SymbolicToPure.ml:1053:4"

Raised at Aeneas__SymbolicToPure.translate_fun_sig_with_regions_hierarchy_to_decomposed.translate_back_inputs_for_gid in file "SymbolicToPure.ml", line 1053, characters 4-49
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Aeneas__SymbolicToPure.translate_fun_sig_with_regions_hierarchy_to_decomposed in file "SymbolicToPure.ml", line 1165, characters 6-62
Called from Aeneas__SymbolicToPure.translate_fun_sig_from_decl_to_decomposed in file "SymbolicToPure.ml", line 1237, characters 4-90
Called from Aeneas__Translate.translate_crate_to_pure.(fun) in file "Translate.ml", line 291, characters 13-99
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 288, characters 6-236
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 992, characters 4-33
Called from Dune__exe__Main in file "Main.ml", line 279, characters 6-58

Just doing:

    let _ = &1 == &1;

is sufficient to cause the crash.

Use continuations for the backward functions

The forward and backward functions lead to some duplication of code, which may lead to duplication in the proofs. A solution would be to make the forward functions return the backward functions as continuations. If we do so, we would also not need to filter the useless forward functions anymore.

It is unclear if doing this is really necessary, and if it would really be more practical to work on functions which return continuations rather than on the tuples (forward function, backward functions), but it is worth experimenting.

This may also make it more practical when working with functions which manipulate a state, when the backward function actually also updates the state (we will need to do so if we want to implement functions such as fn get_mut<T>(address : RawPointer<T>) -> &'a mut T).

Using progress tactic

As discussed offline, here is a simple example where I'm unable to apply the progress tactic:

def foo (a : U32) : Result U32 :=
  do
  let a1 ← a + 1#u32
  if a1 = 2#u32
  then Result.ret 42#u32
  else Result.ret 77#u32

theorem foo_spec (a : U32) : foo a = Result.ret 42#u32 → a = 1#u32 := by
  simp [foo]
  /-
  a : U32
  ⊢ (do
        let a1 ← a + 1#u32
        if a1 = 2#u32 then Result.ret 42#u32 else Result.ret 77#u32) =
      Result.ret 42#u32 →
    a = 1#u32
  -/
  /-
  Progress failed
  -/
  progress

In other cases, the error was of the form: Not an equality: ....

If the theorem doesn't involve an implication, it works, e.g.:

theorem foo_spec2 (a : U32) : foo 1#u32 = Result.ret 42#u32 := by
  simp [foo]
  /-
  a : U32
  ⊢ (do
      let a1 ← 1#u32 + 1#u32
      if a1 = 2#u32 then Result.ret 42#u32 else Result.ret 77#u32) =
    Result.ret 42#u32
  -/
  progress
  /-
  case intro.intro
  a x✝ : U32
  _✝ : x✝.val = 1#u32.val + 1#u32.val
  ⊢ (if x✝ = 2#u32 then Result.ret 42#u32 else Result.ret 77#u32) = Result.ret 42#u32
  -/
  simp_all

Improve handling of opaque and external definitions in Coq and Lean

The Coq and Lean backends handle opaque/external definitions in different and unsatisfactory ways today:

• Coq generates assume val declarations for all the opaque declarations
• Lean declares all the opaque declarations in a record, then generates an assume val instance of this record (the initial idea was to use the section Variable mechanism, but there were some issues)

Those two backends should use the same solution, and a more satisfactory one.
There are overall two possibilities:

• we could try to have a "functor" mechanism, by which the non-opaque definitions are grouped into a module which is parameterized by another module, containing the opaque declarations
• we could simply generate an "interface", then leave it to the user to provide an implementation for this interface. This is almost what the Lean backend does today (we could leave it to the user to write the instance of the record)

Add the possibility of writing specifications/proof annotations in the original Rust code and generating theorem statements

Make the type parameters implicit in the generated functions

The generated functions have explicit type parameters, which makes them a bit cumbersome to use in practice: we could make them implicit in most situations. Of course, we have to make sure that we can always type check the generated files. We could do so in a conservative manner, by making sure a function's implicit parameters can always be deduced from its inputs. There are two cases to take into account.

1. We would need to analyze the signature of the function, to check that the type parameters can be deduced from the input arguments. We could simply check that all the type parameters appear in some input arguments. Note that some quite common functions don't satisfy this condition, for instance fn Vec<T>::new() -> Vec<T> doesn't take any inputs. The type parameters which wouldn't appear in the input arguments would be left as explicit.

2. We might need to introduce type ascriptions when creating structure values, if there are conflicts between field names (i.e., two different structure types have fields with the same names). Note that we do use the fact that some provers like Lean leverage typing information to disambiguate such situations (for Lean, we use short names for the fields, which might collide).

Replace unused function inputs with `_`

Example:
The function below doesn't use its argument:

def take_slice (s : Slice U32) : Result Unit :=
  Result.ret ()

It would be better to generate:

def take_slice (_ : Slice U32) : Result Unit :=
  Result.ret ()

The only case we have to be careful about is decreases clauses in F*: those always receive all the input arguments, so we can't use _ for unused inputs in that case.

Update the ways CPS is used in the compiler

The Aeneas compiler is implemented in CPS because we need to progressively build the execution trace (which is in essence a tree with holes). The way the CPS style is currently implemented makes it very hard to get debugging traces when a failure occurs.

Support non-primitive `Copy` types

This code errors with "Not primitively copyable":

fn test<T: Copy>(x: T) {
    let y = x;
    let z = x;
}

This is because charon emits copy(..) operands without extra trait information. Given that rustc already checks that the types are Copy, we can probably ignore copy(..) entirely on the aeneas side of things.

Add String to the Lean library

This is a feature request to extend Aeneas's Lean library with a model of String including functions such as new, is_empty, len, etc.

Print meaningful error messages with code location

For now, whenever Aeneas encounters an error it simply crashes. It would be better to print an error message indicating the reason behind the error and most importantly the part of the code which triggered it.

A first step might simply be to print the file name and the location inside the file.

We also want to be able to run Aeneas in two modes, like Charon:

• do not abort on failure, go as far as possible and eventually generate definitions with holes while reporting errors (better for the user)
• abort on the first error (better for debugging)

Later we might want to have a Rust executable which links itself to the Rust compiler, runs Charon then Aeneas and reports all the error messages in the same session.

Activate the unit tests for Lean

Because there are sorry in the Lean backend, evaluation of the functions generated by Aeneas often gets stuck. For this reason, the unit tests for Lean (the tests generated for the () -> () functions, by leveraging the normalizer) are currently deactivated: once this is fixed, we will need to reactivate the Lean unit tests.

Remove the `admit`s from the backends

Some definitions in the various backends have admits

Use `omega` instead of `linarith` in the `scalar_tac` tactic

The omega tactic seems more performant than linarith, so it is worth at least experimenting. In particular, I wonder how good it is at reasoning about goals which contain both Nat and Int values.

Improve the performance of unit tests in HOL4

The unit tests in HOL4 are slow: investigate and fix this.

Turn Aeneas into a borrow checker

We could turn Aeneas into a borrow checker by printing informative error messages when there is a borrow checking error (or more generally speaking an invalid access, in particular to a bottom value), and not aborting on the first error.

This issue should be solved after #54.

Add the ADT id in the ADT values

The ADT values currently don't contain the ADT id because this id is contained in the type. While this avoids duplication, this is in practice very cumbersome because in order to get the ADT id and its variant (in case of enumerations) we need to match on both the value and is type.

Generated code dependencies

Seems like there is a big part of problems that is based on lacking functions. But there is a certain amount of real problems also.
Test.txt

Fix the HOL4 backend and reactivate the HOL4 tests

Impossible to override provided trait methods

Code:

#[derive(PartialEq)]
struct Foo {
    x: Option<i32>,
}

Output:

$ charon
   Compiling peq v0.1.0 (/home/ubuntu/examples/aeneas/peq)
[ INFO charon_driver::export:106] [gexport]: Generated the file: /home/ubuntu/examples/aeneas/peq/peq.llbc
    Finished release [optimized] target(s) in 0.17s
$ aeneas -backend lean peq.llbc 
[Info ] Imported: peq.llbc
Uncaught exception:
  
  "Assert_failure Extract.ml:2160:2"

Raised at Aeneas__Extract.extract_trait_impl_register_names in file "Extract.ml", line 2160, characters 2-43
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1112, characters 4-88
Called from Dune__exe__Main in file "Main.ml", line 279, characters 6-58

Error with impl parameterized by a trait

The following code snippet triggers an error:

pub trait Ord {}

pub struct AVLTree<T> {
    pub x: T,
}

impl<T: Ord> AVLTree<T> {
    pub fn insert(&mut self) {
        unimplemented!();
    }
}

impl Ord for u32 {}

pub fn test(mut tree: AVLTree<u32>) {
    tree.insert(); // FAILS HERE
}

The error:

Uncaught exception:
  
  (Invalid_argument List.combine)

Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
Called from Charon__Substitute.make_trait_subst in file "charon/src/Substitute.ml", line 186, characters 11-38
Called from Aeneas__InterpreterUtils.instantiate_fun_sig in file "InterpreterUtils.ml", line 511, characters 4-96
Called from Aeneas__InterpreterStatements.eval_transparent_function_call_symbolic_inst in file "InterpreterStatements.ml", line 759, characters 12-103
Called from Aeneas__InterpreterStatements.eval_transparent_function_call_symbolic in file "InterpreterStatements.ml", line 1321, characters 4-57
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__SynthesizeSymbolic.cf_save_snapshot in file "SynthesizeSymbolic.ml", line 197, characters 68-76
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__SynthesizeSymbolic.cf_save_snapshot in file "SynthesizeSymbolic.ml", line 197, characters 68-76
Called from Aeneas__InterpreterStatements.eval_statement.cf_eval_st.cf_assign in file "InterpreterStatements.ml", line 969, characters 29-70
Called from Aeneas__InterpreterPaths.end_loans_at_place in file "InterpreterPaths.ml", line 558, characters 4-10
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__SynthesizeSymbolic.cf_save_snapshot in file "SynthesizeSymbolic.ml", line 197, characters 68-76
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__SynthesizeSymbolic.cf_save_snapshot in file "SynthesizeSymbolic.ml", line 197, characters 68-76
Called from Aeneas__Interpreter.evaluate_function_symbolic in file "Interpreter.ml", line 605, characters 4-71
Called from Aeneas__Translate.translate_function_to_symbolics in file "Translate.ml", line 34, characters 25-77
Called from Aeneas__Translate.translate_function_to_pure in file "Translate.ml", line 52, characters 23-69
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Stdlib__List.map in file "list.ml", line 92, characters 32-39
Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 231, characters 4-127
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 910, characters 4-33
Called from Dune__exe__Main in file "Main.ml", line 277, characters 6-58

Write an installation script

Don't use projectors for structures extracted as tuples

When accessing its fields, do like with tuples and deconstruct the whole structure:

let (x, y, z) = t
...

Add support for closures

Filing this tracking issue for closure support.

Example program:

fn main() {
  let r: Result<i32, i32> = Ok(3);
  let _: Result<i32, i32> = r.map_err(|_| 4);
}

$ charon
   Compiling clos v0.1.0 (/home/ubuntu/examples/aeneas/clos)
[ INFO charon_driver::export:106] [gexport]: Generated the file: /home/ubuntu/examples/aeneas/clos/clos.llbc
    Finished release [optimized] target(s) in 0.16s
$ aeneas -backend lean clos.llbc 
[Info ] Imported: clos.llbc
Uncaught exception:
  
  (Failure "Closures are not supported yet")

Raised at Aeneas__InterpreterExpressions.eval_rvalue_aggregate.compute in file "InterpreterExpressions.ml", line 796, characters 29-77
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterStatements.eval_statement.cf_eval_st.cf_assign in file "InterpreterStatements.ml", line 955, characters 29-70
Called from Aeneas__InterpreterPaths.end_loans_at_place in file "InterpreterPaths.ml", line 558, characters 4-10
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterPaths.end_loans_at_place in file "InterpreterPaths.ml", line 558, characters 4-10
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterStatements.eval_statement.cf_eval_st.cf_assign in file "InterpreterStatements.ml", line 955, characters 29-70
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__Interpreter.evaluate_function_symbolic in file "Interpreter.ml", line 589, characters 4-71
Called from Aeneas__Translate.translate_function_to_symbolics in file "Translate.ml", line 35, characters 25-77
Called from Aeneas__Translate.translate_function_to_pure in file "Translate.ml", line 55, characters 23-69
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 298, characters 4-127
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 992, characters 4-33
Called from Dune__exe__Main in file "Main.ml", line 279, characters 6-58

Double loop compilation error

fn double_loop() {
    let mut i = 0;
    while i < 10 {
        let mut j = 0;
        while j < 10 {
            j += 1;
        }
        i += 1;
    }
}

The function above fails to compile (using charon + aeneas) with error (including also the commands for compilation)

charon --opaque=main --dest=./test/lean --crate test
aeneas test.llbc -backend lean
[Info ] Imported: test.llbc
Uncaught exception:
  
  "Assert_failure PrePasses.ml:217:10"

Raised at Aeneas__PrePasses.remove_loop_breaks.replace_breaks_with.object#visit_Loop in file "PrePasses.ml", line 217, characters 10-35
Called from Charon__LlbcAst.iter_statement#visit_Loop in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.pp_statement.__1 in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.iter_statement#visit_Loop in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.pp_statement.__1 in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.iter_statement#visit_Loop in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.pp_statement.__1 in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.iter_statement#visit_Loop in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.pp_statement.__1 in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.iter_statement#visit_Loop in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.pp_statement.__1 in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.iter_statement#visit_Loop in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.pp_statement.__1 in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.iter_statement#visit_Loop in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.pp_statement.__1 in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.iter_statement#visit_Loop in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.map_statement#visit_Loop in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.iter_statement#visit_Loop in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Aeneas__PrePasses.remove_loop_breaks.object#visit_Sequence in file "PrePasses.ml", line 237, characters 12-41
Called from Charon__LlbcAst.iter_statement#visit_Loop in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.pp_statement.__1 in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.iter_statement#visit_Loop in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.pp_statement.__1 in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Charon__LlbcAst.iter_statement#visit_Loop in file "src/LlbcAst.ml", line 7, characters 0-1023
Called from Aeneas__PrePasses.remove_loop_breaks in file "PrePasses.ml", line 245, characters 43-75
Called from Stdlib__Map.Make.map in file "map.ml", line 304, characters 19-22
Called from Stdlib__Map.Make.map in file "map.ml", line 305, characters 19-26
Called from Stdlib__Map.Make.map in file "map.ml", line 303, characters 19-26
Called from Stdlib__Map.Make.map in file "map.ml", line 303, characters 19-26
Called from Stdlib__Map.Make.map in file "map.ml", line 305, characters 19-26
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Aeneas__PrePasses.apply_passes in file "PrePasses.ml", line 425, characters 4-96
Called from Dune__exe__Main in file "Main.ml", line 271, characters 14-45
make[1]: *** [aeneas] Error 2
make: *** [test] Error 2

A crash when using derive Hash

Code:

#[derive(Hash)]
struct Foo(u32);

Output:

$ charon
   Compiling hash_val v0.1.0 (/home/ubuntu/examples/aeneas/hash_val)
[ INFO charon_driver::export:106] [gexport]: Generated the file: /home/ubuntu/examples/aeneas/hash_val/hash_val.llbc
    Finished release [optimized] target(s) in 0.17s
$ aeneas -backend lean hash_val.llbc 
[Info ] Imported: hash_val.llbc
Uncaught exception:
  
  (Invalid_argument List.combine)

Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
Called from Charon__Substitute.make_type_subst in file "charon/src/Substitute.ml", line 152, characters 11-35
Called from Aeneas__InterpreterUtils.instantiate_fun_sig in file "InterpreterUtils.ml", line 500, characters 4-73
Called from Aeneas__InterpreterStatements.eval_transparent_function_call_symbolic_inst in file "InterpreterStatements.ml", line 805, characters 20-121
Called from Aeneas__InterpreterStatements.eval_transparent_function_call_symbolic in file "InterpreterStatements.ml", line 1302, characters 4-57
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterStatements.eval_statement.cf_eval_st.cf_assign in file "InterpreterStatements.ml", line 955, characters 29-70
Called from Aeneas__InterpreterPaths.end_loans_at_place in file "InterpreterPaths.ml", line 558, characters 4-10
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterStatements.eval_statement.cf_eval_st.cf_assign in file "InterpreterStatements.ml", line 955, characters 29-70
Called from Aeneas__InterpreterPaths.end_loans_at_place in file "InterpreterPaths.ml", line 558, characters 4-10
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterStatements.eval_statement.cf_eval_st.cf_assign in file "InterpreterStatements.ml", line 955, characters 29-70
Called from Aeneas__InterpreterPaths.end_loans_at_place in file "InterpreterPaths.ml", line 558, characters 4-10
Called from Aeneas__InterpreterExpansion.expand_symbolic_value_no_branching.cc in file "InterpreterExpansion.ml", line 535, characters 19-25
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.greedy_expand_symbolics_with_borrows.expand in file "InterpreterExpansion.ml", line 646, characters 6-12
Called from Aeneas__InterpreterExpansion.expand_symbolic_value_borrow in file "InterpreterExpansion.ml", line 419, characters 17-23
Called from Aeneas__InterpreterExpansion.expand_symbolic_value_shared_borrow in file "InterpreterExpansion.ml", line 386, characters 13-19
Called from Aeneas__Interpreter.evaluate_function_symbolic in file "Interpreter.ml", line 589, characters 4-71
Called from Aeneas__Translate.translate_function_to_symbolics in file "Translate.ml", line 35, characters 25-77
Called from Aeneas__Translate.translate_function_to_pure in file "Translate.ml", line 55, characters 23-69
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 298, characters 4-127
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 992, characters 4-33
Called from Dune__exe__Main in file "Main.ml", line 279, characters 6-58

The following also causes the same crash:

use std::hash::{Hash};
use std::collections::hash_map::DefaultHasher;

fn main() {
    let mut hasher = DefaultHasher::new();
    0.hash(&mut hasher);
}

Crash when translating `Vec::dedup`

Using Vec::dedup triggers a crash:

fn use_dedup<T:PartialEq>(v: &mut Vec<T>) {
  v.dedup()
}

Allow types to be parameterized by traits

The following is currently not accepted:

struct S<T : Ord> { x : T }

Match on integer produces invalid Lean

The following Rust function:

fn foo(x: i32) -> bool {
    match x {
        0 => true,
        _ => false
    }
}

produces:

/- [match_i32::foo]:
   Source: 'src/main.rs', lines 1:0-1:22 -/
def foo (x : I32) : Result Bool :=
  match x with
  /-
  invalid pattern, constructor or constant marked with '[match_pattern]' expected
  -/
  | 0#i32 => Result.ret true
  | _ => Result.ret false

Lean complains about the 0#i32 with the error shown in the comment.

Improve the names for the backward functions

Names like back_'a are not very pretty: back'a would be better.
Also, when calling a function, we sometimes name back a value (i.e., a backward function with no inputs), which is a bit confusing.

Name clash detected error when method and trait method have the same name

For the following program:

trait T {
    fn f(&self);
}

struct Foo {
    x: i32,
}

impl Foo {
    fn f(&self) { }
}

impl T for Foo {
    fn f(&self) { }
}

fn main() { }

Aeneas complains of a name clash:

$ charon
   Compiling clash v0.1.0 (/home/ubuntu/examples/aeneas/clash)
[ INFO charon_driver::export:106] [gexport]: Generated the file: /home/ubuntu/examples/aeneas/clash/clash.llbc
    Finished release [optimized] target(s) in 0.15s
$ aeneas -backend lean clash.llbc 
[Info ] Imported: clash.llbc
[Error] Name clash detected: the following identifiers are bound to the same name "Foo.f":
- clash::{clash::Foo}::f
- clash::{clash::Foo#1}::f
You may want to rename some of your definitions, or report an issue.
Uncaught exception:
  
  (Failure
    "Name clash detected: the following identifiers are bound to the same name \"Foo.f\":\
   \n- clash::{clash::Foo}::f\
   \n- clash::{clash::Foo#1}::f\
   \nYou may want to rename some of your definitions, or report an issue.")

Raised at Aeneas__ExtractBase.report_name_collision in file "ExtractBase.ml", line 266, characters 28-47
Called from Aeneas__ExtractBase.names_map_add in file "ExtractBase.ml", line 291, characters 2-51
Called from Aeneas__ExtractBase.names_maps_add in file "ExtractBase.ml", line 422, characters 20-67
Called from Aeneas__ExtractBase.ctx_add in file "ExtractBase.ml", line 662, characters 19-69
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 997, characters 4-761
Called from Dune__exe__Main in file "Main.ml", line 274, characters 6-58

Using the same name is legal in Rust: https://doc.rust-lang.org/book/ch19-03-advanced-traits.html#fully-qualified-syntax-for-disambiguation-calling-methods-with-the-same-name