aeneasverif/charon

Interface with the rustc compiler for the purpose of program verification

Patinir, E., 1515-1524, Landscape with Charon crossing the Styx [Oil on wood]. Museo del Prado, Madrid. Source

Charon

Charon acts as an interface between the rustc compiler and program verification projects. Its purpose is to process Rust crates and convert them into files easy to handle by program verifiers. It is implemented as a custom driver for the rustc compiler.

Charon is, in Greek mythology, an old man carrying the souls of the deceased accross the Styx, a river separating the world of the living from the world of the dead. In the present context, Charon allows us to go from the world of Rust programs to the world of formal verification.

We are open to contributions! Please contact us so that we can coordinate ourselves, if you are willing to contribute. For this purpose you can join the Zulip.

LLBC

Charon converts MIR code to ULLBC (Unstructured Low-Level Borrow Calculus) then to LLBC. Both ASTs can be output by Charon.

ULLBC is a slightly simplified MIR, where we try to remove as much redundancies as possible. For instance, we drastically simplify the representation of constants coming from the Rust compiler.

LLBC is ULLBC where we restructured the control-flow with loops, if ... then ... else ..., etc. instead of gotos. Consequently, we merge MIR statements and terminators into a single LLBC statement type. We also perform some additional modifications, some of which are listed below:

Remark: most of the transformations which transform the MIR to ULLBC then LLBC are implemented by means of micro-passes. Depending on the need, we could make them optional and control them with flags. If you want to know more about the details, see translate in src/driver.rs, which applies the micro-passes one after the other.

Remark: if you want to know the full details of (U)LLBC, have a look at: types.rs, values.rs, expressions.rs, ullbc_ast.rs and llbc_ast.rs.

The extracted AST is serialized in .ullbc and .llbc files (using the JSON format). We extract a whole crate in one file.

Project Structure

• charon: the Rust implementation.
• charon-ml: the ML library. Provides utilities to retrieve and manipulate the AST in OCaml (deserialization, printing, etc.).
• tests and tests-polonius: test files directories. tests-polonius contains code which requires the Polonius borrow checker.

Installation & Build

You first need to install rustup.

As Charon is set up with cargo, rustup will automatically download and install the proper packages upon building the project. If you only want to build the Rust project (in ./charon), simply run make build-charon-rust in the top directory.

If you also want to build the ML library (in ./charon-ml), you will need to install OCaml and the proper dependencies.

We suggest you to follow those instructions, and install OPAM on the way (same instructions).

For Charon-ML, we use OCaml 4.13.1: opam switch create 4.13.1+options

The dependencies can be installed with the following command:

opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc menhir

You can then run make build-charon-ml to build the ML library, or even simply make to build the whole project (Rust and OCaml). Finally, you can run the tests with make test.

Alternatively, you can use Nix and do nix develop (or use https://direnv.net/ and direnv allow) and all dependencies should be made available.

Documentation

If you run make, you will generate a documentation accessible from doc-rust.html (for the Rust project) and doc-ml.html (for the ML library).

Usage

To run Charon, you should run the Charon binary from within the crate that you want to compile, as if you wanted to build the crate with cargo build. The Charon executable is located at bin/charon.

Charon will build the crate and its dependencies, then extract the AST. Charon provides various options and flags to tweak its behaviour: you can display a detailed documentation with --help. In particular, you can print the LLBC generated by Charon with --print-llbc.

Remark: because Charon is compiled with Rust nigthly (this is a requirement to implement a rustc driver), it will build your crate with Rust nightly. You can find the nightly version pinned for Charon in rust-toolchain.template.

charon's Issues

Add support for spec annotations

It would be good to add the possibility of annotating the definitions with pre/post-conditions and even proof annotations.
This issue should be done after #63

Add support for constant slices

This generates an error:

const S: &str = "Hello";

Error:

Unsupported constant: "ConstValue::Slice: Slice { data: ConstAllocation { .. }, start: 0, end: 98 }"

Update the CI to format the code and check that there are no compilation warnings

Def Ids: handle the case `ForeignMod`

The case ForeigMod is not handled by names_utils::extended_def_id_to_name

Use a `Vec` in `RawStatement::Sequence`

Currently it takes a pair of statements, which isn't very practical to pattern-match on. If it was a Vec, we could use slice patterns which should be a lot more convenient.

The drawback is we can't move out of a slice pattern, so we'll either have to clone or insert/remove on the Vec.

Compilation hangs when having a type defined inside a trait

The following code snippet

pub trait Trait1 {
    type T: Trait2;
}

pub trait Trait2: Trait1 {
    type T;
}

makes charon hang. The motivation for this structure can be found in arkworks/ff.

Traits breaks Charon

Using the Debug or Clone trait breaks Charon. Looking at the code that fails I expect that any trait will make Charon panic really.

pub fn trait_error(s: &[u8]) {
  let _array: [u8; 4] = s.try_into().unwrap();
}

produces the following error (try_into requires implementation of Debug).

[13:34:02 TRACE charon::generics:105] [check_generics]:
trait_name: core::fmt::Debug
thread 'rustc' panicked at 'assertion failed: trait_name.equals_ref_name(&assumed::MARKER_SIZED_NAME)', src/generics.rs:106:17

Similarly,

pub fn vec_error() {
  let _vec = vec![0u8; 5];
}

produces

[13:46:49 TRACE charon::generics:105] [check_generics]:
trait_name: core::clone::Clone
thread 'rustc' panicked at 'assertion failed: trait_name.equals_ref_name(&assumed::MARKER_SIZED_NAME)', src/generics.rs:106:17

Add span information to structure fields, trait items, etc.

Unsupported statement error when accessing enum discriminat

For the following program:

enum Foo {
    A,
    B,
}

fn main() {
    let x = Foo::A;
    let _y = x as isize;
}

Charon errors out:

$ charon
   Compiling discr v0.1.0 (/home/ubuntu/examples/aeneas/discr)
error: Unsupported statement kind: intrinsic
 --> src/main.rs:8:14
  |
8 |     let _y = x as isize;
  |              ^^^^^^^^^^

[ INFO charon_driver::export:101] [gexport]: Generated the partial (because we encountered errors) file: /home/ubuntu/examples/aeneas/discr/discr.llbc
[ ERROR charon_driver:231] The extraction encountered 1 errors
error: could not compile `discr` (bin "discr") due to previous error

Error with a generic const

For the following Rust program:

struct Foo<T> {
    x: Option<T>,
}

impl<T> Foo<T> {
    const FOO: Result<T, i32> = Err(0);
}

charon errors out:

$ charon
   Compiling const_gen v0.1.0 (/home/ubuntu/examples/aeneas/const_gen)
error: Could not find the type variable "T" (index: 0)
 --> src/main.rs:6:5
  |
6 |     const FOO: Result<T, i32> = Err(0);
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^

error: Ignoring the following global due to an error: DefId(0:8 ~ const_gen[4689]::{impl#0}::FOO)
 --> src/main.rs:6:5
  |
6 |     const FOO: Result<T, i32> = Err(0);
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^

[ INFO charon_driver::export:101] [gexport]: Generated the partial (because we encountered errors) file: /home/ubuntu/examples/aeneas/const_gen/const_gen.llbc
[ ERROR charon_driver:231] The extraction encountered 2 errors
error: could not compile `const_gen` (bin "const_gen") due to 2 previous errors

Doesn't support workspaces

In workspaces the target directory is not in the same directory as the crate. So this will always fail.

https://github.com/Kachoc/charon/blob/7154478ad283b2a8b5fc4a409187c86137505223/charon/src/main.rs#L405

panic in empty function

Getting the length of a slice is not supported.

pub fn some_error(_: &[u8]) {}

produces

[15:00:25 TRACE charon::translate_functions_to_im:2037] [translate_function_signature]:
# Output variable type:
()
thread 'rustc' panicked at 'not implemented', src/regions_hierarchy.rs:352:13

Note that Charon is fine with the following

pub fn no_error() {}

I think a lot of the issues are stemming from the same issue that array and slices aren't supported (regions_hierarchy.rs).

        Ty::Array(_aty) => {
            unimplemented!();
        }
        Ty::Slice(_sty) => {
            unimplemented!();
        }

Misc issues (map, const generic, array updates, assertions)

Here are some issues when trying to run charon on Rust code.

map

pub fn map(x: [i32; 256],) -> [i32; 256] {
    x.map(|v| v)
}

thread 'rustc' panicked at 'not implemented: impl source: ImplSourceClosureData(closure_def_id=DefId(0:6 ~ simplemap[2625]::add::{closure#0}), substs=[i16, extern "rust-call" fn((i32,)) -> i32, ()], nested=[Obligation(predicate=Binder(ClosureKind(DefId(0:6 ~ simplemap[2625]::add::{closure#0}), [i16, extern "rust-call" fn((i32,)) -> i32, ()], FnMut), []), depth=1)])', /Users/franziskus/.cargo/git/checkouts/hacspec-v2-fad44c11f2620bcb/60ef8f9/frontend/exporter/src/types/traits.rs:428:13

const generic

pub fn array<const LEN: usize>() -> [u8; LEN] {
    [0u8; LEN]
}

thread 'rustc' panicked at 'internal error: entered unreachable code: ConstGeneric::as_value: Not the proper variant', src/types.rs:404:56

array update in loops

fn cbd(mut prf_input: [u8; 33]) {
    for i in 0..3 {
        prf_input[0] = i;
    }
}

thread 'rustc' panicked at 'internal error: entered unreachable code: Could not find a clause for parameter:
- target param: @TraitDecl1<Self::IntoIter>
- available clauses:
@TraitDecl0<Self>', src/translate_predicates.rs:599:13

assertions

pub(crate) fn select(lhs: &[u8], rhs: &[u8]) {
    debug_assert_eq!(lhs.len(), rhs.len());
}

thread 'rustc' panicked at 'Unsupported ADT: core::panicking::AssertKind', src/translate_functions_to_ullbc.rs:924:33

Consider adding version numbers in the .llbc files

Right now, charon-ml might fail to load a .llbc file because, say, charon produces a new construct, but charon-ml does not (yet) know how to read it. Or, worse, a .llbc file is stale (old), and charon-ml is recent, and the .llbc file has not been regenerated properly, which means that there is a version mismatch.

Version numbers might help providing a useful error message, and figure out the discrepancy.

Remove the ULLBC

Represent data type constructors with strings instead of variant ids

A note about this piece of code:

charon/charon/src/translate_functions_to_ullbc.rs

Lines 1308 to 1366 in 99e3013

	if adt_id.is_local() {
	// Local ADT: retrieve the definition
	let id_t = *bt_ctx.ft_ctx.ordered.type_rid_to_id.get(adt_id).unwrap();
	let def = bt_ctx.get_type_defs().get_type_def(id_t).unwrap();
	assert!(region_params.len() == def.region_params.len());
	assert!(type_params.len() == def.type_params.len());
	let variant_id = match &def.kind {
	ty::TypeDeclKind::Enum(variants) => {
	let variant_id = translate_variant_id(*variant_idx);
	assert!(
	operands_t.len()
	== variants.get(variant_id).unwrap().fields.len()
	);
	Some(variant_id)
	}
	ty::TypeDeclKind::Struct(_) => {
	assert!(variant_idx.as_usize() == 0);
	None
	}
	ty::TypeDeclKind::Opaque => {
	unreachable!("Can't build an aggregate from an opaque type")
	}
	};
	let akind =
	e::AggregateKind::Adt(id_t, variant_id, region_params, type_params);
	e::Rvalue::Aggregate(akind, operands_t)
	} else {
	// External ADT.
	// Can be `Option`
	// TODO: treat all external ADTs in a consistant manner.
	// For instance, we can access the variants of any external
	// enumeration marked as `public`.
	let name = type_def_id_to_name(tcx, *adt_id);
	assert!(name.equals_ref_name(&assumed::OPTION_NAME));
	// Sanity checks
	assert!(region_params.is_empty());
	assert!(type_params.len() == 1);
	// Find the variant
	let variant_id = translate_variant_id(*variant_idx);
	if variant_id == assumed::OPTION_NONE_VARIANT_ID {
	assert!(operands_t.is_empty());
	} else if variant_id == assumed::OPTION_SOME_VARIANT_ID {
	assert!(operands_t.len() == 1);
	} else {
	unreachable!();
	}
	let akind =
	e::AggregateKind::Option(variant_id, type_params.pop().unwrap());
	e::Rvalue::Aggregate(akind, operands_t)
	}

Right now, there are two code-paths for translating data types constructor applications.

• If we have access to the definition of the data type (it is "local"), then we look up the definition of the data type, then compute a variant id, which is essentially the index of the variant in the data type definition, and represent the constructor application as AggregateKind::Adt which takes a type identifier, followed by a variant identifier
• If we do not have access to the definition of the data type (it is not local), then it must be one of the few built-in types we know how to handle. One such type is Option, for which we hardwire the knowledge that the VariantId of None is 0, and that the VariantId of Some is 1. (My most recent PR adds Range as another builtin type.)

The main issue with this translation scheme is that we cannot handle non-local (a.k.a. opaque) types in a generic fashion, because we need that map from constructor to VariantId.

A possible solution (to be discussed) is to represent variants with mere names (i.e., strings), which would then allow for a single translation scheme, regardless of whether the definition is available or not.

@sonmarcho do you remember why VariantId's are important?

Add support for quantified lifetimes (`for <'a>`)

For now Charon does not support quantified lifetimes, as indicated by for <'a> ... in the where clauses.

Fix a warning during the build

Dependency lookup is broken

It looks like the dependency lookup isn't implementing the -/_ replacement in crate names and thus can't find dependencies with a - in the name.

https://github.com/Kachoc/charon/blob/7154478ad283b2a8b5fc4a409187c86137505223/charon/src/main.rs#L464

`cargo-charon` fails to parse arguments correctly

Cargo version: cargo 1.66.0-nightly (7e484fc1a 2022-10-27)

I installed cargo-charon as a Cargo CLI extension using cargo install. Invoking cargo charon fails for me on a simple repository due to what appears to be an argument-parsing error:

error: Found argument 'charon' which wasn't expected, or isn't valid in this context

USAGE:
    cargo-charon [FLAGS] [OPTIONS]

For more information try --help

Manually running the cargo-charon executable from where Cargo installed it to works as expected.

---

I took the above approach because the executable is named like a Cargo plugin, and because the documentation suggests something which no longer works (cargo run errors out due to the lack of a default executable.) If cargo-charon isn't meant to be installed like this, I'm happy to update the docs in some way.

Extract inlining information

This issue will probably require #63

Get rid of the Makefiles

The Makefiles are getting bloated, especially for the tests, and are hard to maintain especially for people who are not used to writing makefiles. It would be better to have a script file or, probably better, only rely on cargo.

Rename `Meta` to `SpanMeta`

As suggested here, to disambiguate with ItemMeta.

Binary location

README.md says the charon executable is located at bin/charon. On my machine, I found it at charon/target/debug/charon. I am using OSX, and built charon using gmake build-charon-rust.

Add support for mutually recursive trait definitions

Mutually recursive traits happen in practice, for example here (mutual recursion between PrimeField and Field):

pub trait Trait1 {
    type T: Trait2;
}

pub trait Trait2: Trait1 {}

It would be good to handle those, or at least print a nice error message. For now, Charon panics with:

thread 'rustc' panicked at 'Invalid trait decl group:
tests4::Trait1
tests4::Trait2', src/reorder_decls.rs:116:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
error: could not compile `tests4` (bin "tests4")

Extract visibility information

We need to extract visibility information like pub or pub(crate), etc.

Non-positive indexes for variants are unhandled

Consider:

enum Ordering {
    Lesser  = -1,
    Equal = 0,
    Greater = 1
}

(taken from https://github.com/RaitoBezarius/avl-verification/blob/main/src/main.rs)

Charon will crash because it will generate a usize::MAX - 1 > u32::MAX for https://github.com/RaitoBezarius/avl-verification/blob/main/src/main.rs#L29 variant in the pattern matching.

Add support for iter next

Filing this tracking issue for unsupported predicates with bound regions.

This is an example program that triggers the issue:

fn main() {
    let a = [1, 2, 3];
    let _x = a.iter().next();
}

$ charon
   Compiling any v0.1.0 (/home/ubuntu/examples/aeneas/any)
error: Predicates with bound regions (i.e., `for<'a> ...`) are not supported yet
   --> /home/ubuntu/.rustup/toolchains/nightly-2023-06-02-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter.rs:131:1
    |
131 | / iterator! {struct Iter -> *const T, &'a T, const, {/* no mut */}, {
132 | |     fn is_sorted_by<F>(self, mut compare: F) -> bool
133 | |     where
134 | |         Self: Sized,
...   |
138 | |     }
139 | | }}
    | |__^
    |
    = note: this error originates in the macro `iterator` (in Nightly builds, run with -Z macro-backtrace for more info)

error: Ignoring the following function due to an error: DefId(2:42967 ~ core[6c80]::slice::iter::{impl#181}::find)
   --> /home/ubuntu/.rustup/toolchains/nightly-2023-06-02-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter.rs:131:1
    |
131 | / iterator! {struct Iter -> *const T, &'a T, const, {/* no mut */}, {
132 | |     fn is_sorted_by<F>(self, mut compare: F) -> bool
133 | |     where
134 | |         Self: Sized,
...   |
138 | |     }
139 | | }}
    | |__^
    |
    = note: this error originates in the macro `iterator` (in Nightly builds, run with -Z macro-backtrace for more info)

error: Predicates with bound regions (i.e., `for<'a> ...`) are not supported yet
   --> /home/ubuntu/.rustup/toolchains/nightly-2023-06-02-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter.rs:135:12
    |
135 |         F: FnMut(&Self::Item, &Self::Item) -> Option<Ordering>,
    |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: Ignoring the following function due to an error: DefId(2:42977 ~ core[6c80]::slice::iter::{impl#181}::is_sorted_by)
   --> /home/ubuntu/.rustup/toolchains/nightly-2023-06-02-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter.rs:132:5
    |
132 | /     fn is_sorted_by<F>(self, mut compare: F) -> bool
133 | |     where
134 | |         Self: Sized,
135 | |         F: FnMut(&Self::Item, &Self::Item) -> Option<Ordering>,
    | |_______________________________________________________________^

error: The external definition DefId(2:42977 ~ core[6c80]::slice::iter::{impl#181}::is_sorted_by) triggered errors. It is (transitively) used at the following location(s):
 --> src/main.rs:3:14
  |
3 |     let _x = a.iter().next();
  |              ^^^^^^^^^^^^^^^

error: The external definition DefId(2:42967 ~ core[6c80]::slice::iter::{impl#181}::find) triggered errors. It is (transitively) used at the following location(s):
 --> src/main.rs:3:14
  |
3 |     let _x = a.iter().next();
  |              ^^^^^^^^^^^^^^^

[ INFO charon_driver::export:101] [gexport]: Generated the partial (because we encountered errors) file: /home/ubuntu/examples/aeneas/any/any.llbc
[ ERROR charon_driver:231] The extraction encountered 4 errors
error: could not compile `any` (bin "any") due to 6 previous errors

`assertion failed: int_ty.is_isize()` when deriving `PartialOrd`

For the following program:

#[derive(PartialEq, PartialOrd)]
struct Foo {
    x: i32,
    y: i32,
}

fn main() { }

charon crashes as follows:

$ RUST_BACKTRACE=1 charon
   Compiling ord v0.1.0 (/home/ubuntu/examples/aeneas/ord)
thread 'rustc' panicked at 'assertion failed: int_ty.is_isize()', src/remove_read_discriminant.rs:56:17
stack backtrace:
   0: rust_begin_unwind
             at /rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/std/src/panicking.rs:593:5
   1: core::panicking::panic_fmt
             at /rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/panicking.rs:67:14
   2: core::panicking::panic
             at /rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/panicking.rs:117:5
   3: charon_driver::remove_read_discriminant::Visitor::update_statement
   4: charon_driver::llbc_ast_utils::MutAstVisitor::default_visit_raw_statement
   5: charon_driver::llbc_ast_utils::MutAstVisitor::default_visit_raw_statement
   6: charon_driver::translate_ctx::TransCtx::iter_bodies
   7: charon_driver::driver::translate
   8: <charon_driver::driver::CharonCallbacks as rustc_driver_impl::Callbacks>::after_parsing
   9: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_span::ErrorGuaranteed>>
  10: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_span::ErrorGuaranteed>>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
error: could not compile `ord` (bin "ord")

Detect overflow checks properly

After #124, there's still a case where we don't detect overflow checks properly:

fn div_signed_with_constant() -> i32 {
    const FOO: i32 = 42;
    FOO / 2
}

gives:

fn test_crate::div_signed_with_constant() -> i32
{
    let @0: i32; // return
    let @1: bool; // anonymous local
    let @2: bool; // anonymous local
    let @3: i32; // anonymous local
    let @4: i32; // anonymous local

    @1 := const (2 : i32) == const (-1 : i32)
    @3 := test_crate::div_signed_with_constant::FOO
    @2 := move (@3) == const (-2147483648 : i32)
    @4 := test_crate::div_signed_with_constant::FOO
    @0 := move (@4) / const (2 : i32)
    return
}

because the constants are inserted in the middle of the checks.

Add an option to extract the bodies of the external definitions

For now, whenever possible we treat foreign definitions as opaque, that is we treat all external functions as opaque and thus don't look at their bodies, treat external structures without public fields as opaque, etc. It is sometimes useful to extract the bodies of the external definitions, and Eurydice needs this: we need to add a CLI option for this. Also, it might be good to be able to tweak this behavior, for instance by extracting only the bodies of the functions marked as #[inline], etc.

Make the ScalarValue::Isize and Usize variants use i64 and u64 instead of isize/usize

In values.rs we have:

pub enum ScalarValue {
    Isize(isize),
    Usize(usize),
    ...
}

This doesn't work if we do cross-compilation: we should use i64 and u64 to store the integer values.

Add support for attributes

It would be good to have the possibility of annotating the Rust definitions with attributes, for instance to mark some definitions as opaque, to tweak the name of the definitions for the extraction, etc.

Support `Rvalue::Discriminant` not followed by `SwitchInt`

This can show up in optimized MIR, for example the optimized mir of Option::is_some(). It's not too hard to support: we can replace _x = Discriminant(_y) with

match _y {
    Variant1 => _x = <disciminant value for variant 1>,
    ...
}

Turn charon into a subcommand

We want to be able to run cargo charon

Update the comment for `TypesUtils.ty_is_copyable`

charon/charon-ml/src/TypesUtils.ml

Line 209 in a0c861c

* traits.

The comment should explain why we keep the function:

• it is used in the code of Aeneas exactly where we need to check that a type is copyable
• for now we don't do the check (as the function always returns true) but we might want to do something more precise in the future.
• if we do so, it is good not to have to dive in the code to notice where we should reinsert the checks, because we would likely miss some

Add support for quantified where clauses

For now, quantified where clauses like below are not supported:

where for<'a> Foo : Bar<'a>

from_le_bytes not usable

Trying to convert u8 to u32 breaks.

pub fn builtin_error(s: [u8; 4]) {
  let _value = u32::from_le_bytes(s);
}

produces

[13:37:11 TRACE charon::names_utils:124] [item_def_id_to_name]:
DefId(2:25039 ~ core[1586]::num::{impl#8}::from_le_bytes)
thread 'rustc' panicked at 'internal error: entered unreachable code', src/names_utils.rs:230:25

Ignore dev-dependencies

Charon appears to expect dev-dependencies to be compiled, i.e. running cargo build is not enough.
If this is intentional, the recommendation should be changed to run cargo build --tests or a switch could be added to not look at tests.

Add support for `dyn Trait`

Support for for-loops

Ended up hitting this code today:

  for j in 0..256 {
    r[j] = fqmul(r[j], F);
  }

This is not currently supported because it relies on an iterator trait, and we don't support traits. Rather than do a lot of peephole optimizations in Charon to recognize this and extract it as a dedicated AST for node, we suggest:

• supporting traits, in general
• adding an optional phase in charon-ml that takes care of pattern-matching on this particular usage of traits and rewriting it into a dedicated high-level For AST node

Add `StatementKind::Error`

For cases like in #107 where a pass fails.