Getting Started

Charon is a CLI tool that helps other tools analyze Rust code. Its basic function is that you call charon cargo on a Rust crate, and Charon produces a file which contains all the information you could possibly hope to get from the crate¹.

This manual is a bare-bones draft that we plan to improve over time. In the meantime, if there’s something you want to know about, come ask on Zulip!

Project Status

Charon is under active development, with one engineer (Nadrieril) employed full-time to work on it. It is currently beta software, i.e. without major known bugs and nearing a complete feature set. We’re working towards a 1.0, once we settle the last remaining design points, document everything, and finish a couple features.

Charon supports all Rust features except async (tracked here).

Semantic information only however; we do not preserve syntactic information like scopes nor distinguish say while from loop. ↩

Installation

Note

This is about installing the Charon binary. There is no tutorial yet for the OCaml or Rust libraries.

Charon is available via several channels: prebuilt binaries, Nix, and building from source.

Prebuilt Binaries

Charon provides prebuilt binaries for Linux (aarch64, x86_64) and macOS (aarch64). You can download the latest release from the GitHub releases page.

Nix

To install Charon through Nix, just run:

nix run github:AeneasVerif/charon

Building from Source

Charon may also be built from source. First, you will need to have rustup installed. Make sure you don’t have pre-existing Rust or Cargo installations through means other than rustup (e.g. brew), as this can cause issues with the build.

Then, clone the repository and run the following commands. The resulting binary will be in bin/charon:

git clone https://github.com/AeneasVerif/charon.git
cd charon
make build-charon-rust

Usage

To run Charon, you should run the charon cargo from within the crate that you want to compile, as if you wanted to build the crate with cargo build.

Charon will build the crate and its dependencies, then extract the crate contents. Charon provides various options and flags to tweak its behaviour: you can display a detailed documentation with --help. In particular, you can pretty-print the translated crate with both --print-ullbc and --print-llbc, depending on the Charon intermediate representation you wish to use.

Charon supports per-crate configuration via the [package.metadata.charon] section in Cargo.toml. The exact list can be found by looking at src/bin/charon/toml_config.rs. If an option is set both as a CLI flag and as a toml value and we can’t merge them, the CLI flag wins.

Remark: because Charon is compiled with Rust nightly (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.

Names

Each item (function, trait decl, type decl etc) in Charon has a unique name, that looks like a Rust path (e.g., std::boxed::Box). This name can be used to uniquely identify items using patterns.

These patterns are used most notably for the --include/--exclude cli options, and made available in Rust and OCaml with NameMatcher. Caveat: the Rust and OCaml name matchers differ in input syntax and behavior; this is tracked in https://github.com/AeneasVerif/charon/issues/319.

TODO: explain syntax and behavior.

Note: for well-known built-in items, you can often use ItemMeta.lang_item instead; it contains an identifier meant for this purpose, documented here.

CLI options

TODO: explain the main options, and LLBC vs ULLBC

In short: LLBC is the name we give to the output of Charon. It stands for Low-Level Borrow Calculus and is the name used in the formalisations of the Aeneas project. Charon was initially created as part of the Aeneas project, and therefore inherits that name. ULLBC means Unstructured LLBC, i.e., LLBC without the control-flow reconstruction.

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.

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 transformation_passes in src/bin/charon-driver/driver.rs, which applies the micro-passes one after the other.

Running Charon on Rust-for-Linux’s `kernel` crate

Rust-for-Linux’s kernel crate is built by Kbuild rather than Cargo. Running Charon on it requires some acrobatics.

You must be able to build the kernel crate, and have charon in your PATH.

Setup

The following assumes that the current directory is a clone of the kernel.

Pick an output path and some options to pass to Charon:

$ export CHARON_OUTPUT="$PWD/kernel.llbc"
$ export CHARON_OPTIONS="--extract-opaque-bodies --monomorphize"

Find Charon and the toolchain it needs:

$ export CHARON_BIN="$(command -v charon)"
$ export CHARON_RUSTC="$(charon toolchain-path)/bin/rustc"

Prepare a build directory and enable rust support:

$ mkdir -p ../linux-build
$ export KERNEL_BUILD_DIR="$(realpath ../linux-build)"
$ make LLVM=1 O="$KERNEL_BUILD_DIR" RUSTC="$CHARON_RUSTC" rustavailable
$ make LLVM=1 O="$KERNEL_BUILD_DIR" RUSTC="$CHARON_RUSTC" defconfig
$ scripts/config --file "$KERNEL_BUILD_DIR/.config" -e RUST
$ make LLVM=1 O="$KERNEL_BUILD_DIR" RUSTC="$CHARON_RUSTC" olddefconfig

Write the following script to $KERNEL_BUILD_DIR/charon-rustc:

#!/usr/bin/env sh
set -eu

is_kernel=false
previous=
for argument in "$@"; do
    if [ "$previous" = "--crate-name" ] && [ "$argument" = "kernel" ]; then
        is_kernel=true
        break
    fi
    previous=$argument
done

if [ "$is_kernel" = true ]; then
    export CHARON_EMIT_ARTIFACTS=1
    exec "$CHARON_BIN" rustc \
        $CHARON_OPTIONS \
        --sysroot default \
        --dest-file "$CHARON_OUTPUT" \
        -- "$@"
else
    exec "$CHARON_RUSTC" "$@"
fi

and make it executable:

$ chmod +x "$KERNEL_BUILD_DIR/charon-rustc"

The wrapper acts just like rustc except that if we’re compiling a crate called kernel, it will also extract it via Charon into the $CHARON_OUTPUT file.

Run Charon

Build the kernel crate with the wrapper:

$ touch rust/kernel/lib.rs
$ make LLVM=1 \
    O="$KERNEL_BUILD_DIR" \
    RUSTC="$KERNEL_BUILD_DIR/charon-rustc" \
    rust/kernel.o

The output llbc file can then be found in $CHARON_OUTPUT.

For example, the layout of Linux’s C struct list_head can be inspected with:

$ charon pretty-print --include-layouts "$CHARON_OUTPUT" > kernel.pretty
$ rg -A24 \
    'Full name: bindings::bindings_raw::list_head$' \
    kernel.pretty

Charon item selection

Items and opacity

An item is a module, function, type decl, static, const, trait decl, or trait impl. A crate is considered a module.

Each item has an opacity level¹:

Transparent — the item is fully translated.
Foreign — the default for items outside the current crate. Translation depends on normal Rust visibility: for types, translate fully if it’s a struct with all-public fields or an enum; for other items this is equivalent to Opaque.
Opaque — only the name and signature are translated, not the contents. For functions and globals, the body is not translated. For types (structs, enums, unions), the fields/variants are not translated. For traits and trait impls, methods with a default body are only translated if mentioned (used or overridden) anywhere in the final crate. For modules, the contents are not explored (but items referenced from elsewhere are still translated).
Invisible — nothing is translated for this item. The corresponding map will not have an entry for the item ID. Useful when even the signature causes errors.

Selection process

Charon starts from a set of entry points and explores outward using a work-queue:

The entry point items are enqueued for processing.
Each item is processed according to its opacity:
- Transparent module: enqueue all items directly inside it.
- Non-transparent module: do nothing (contents are not explored).
- Transparent non-module item: translate it fully (including body).
- Foreign or opaque non-module item: translate only the signature.
- Invisible item: do nothing.
Whenever processing an item encounters a reference to a new item, that new item is enqueued for processing.

This is a dependency-driven algorithm that pulls in items as they are needed. With the default settings, the entry point is the current crate (a module), which is transparent, so all its direct items are enqueued. Those items reference foreign items from dependencies, which get enqueued as foreign (signatures only). The result: the whole current crate is translated, plus the signatures of all foreign items it references.

Opacity vs reachability: An item’s opacity (how much of it is translated) is determined solely by its own name and annotations — it does not inherit from the item that references it. But reachability (whether the item is queued at all) does depend on the exploration path: an item only reachable through an opaque item’s body will not be queued, since opaque bodies are not explored. In the default setup (the whole crate as a transparent entry point), all current-crate items are enqueued via module traversal regardless of call-graph structure. This distinction matters mainly when using custom --start-from patterns or opaque modules.

How opacity is determined

Each item’s opacity is calculated from its name by matching against a list of patterns. The patterns come from two sources: CLI flags and source annotations.

Source annotations

The source-level attributes #[charon::opaque] and #[charon::exclude] set the opacity of individual items. They can only make items more opaque, never less².

When both a source annotation and a CLI pattern apply, the more opaque of the two wins (Transparent < Foreign < Opaque < Invisible). This means --include cannot override a #[charon::opaque] annotation.

Scope difference: #[charon::opaque] applies only to the annotated item itself. Items nested within it — functions in a module, methods in an impl block — are separate items with their own opacity, which for current-crate items defaults to Transparent. By contrast, --opaque crate::module uses prefix matching³, so it makes crate::module and every item whose path starts with crate::module (e.g. crate::module::foo) Opaque.

Concretely: if a module is annotated #[charon::opaque], a function inside it that is called from outside the module will still be translated fully (body included), because the function’s own opacity is Transparent. Using --opaque crate::that_module instead would make that nested function Opaque (signature only).

CLI flags

--start-from <PATTERN> — Entry points for translation. Can be specified multiple times. Default: crate (the entire current crate).
--start-from-attribute[=<ATTR>] — Use items annotated with a given attribute as entry points. Default attribute if none specified: verify::start_from.
--start-from-pub — Use all pub items from the current crate as entry points
--include <PATTERN> — Set matched items to transparent.
--opaque <PATTERN> — Set matched items to opaque.
--exclude <PATTERN> — Set matched items to invisible.
--extract-opaque-bodies — Makes all items transparent. Internally changes the base pattern from _ → Foreign to _ → Transparent (see Pattern list below), so it affects all items including external ones.
--translate-all-methods — Include provided trait methods even if unused. Equivalent to making all trait declarations transparent.

Pattern list

Charon builds an ordered list of (pattern, opacity) pairs from the CLI flags⁴:

_              → Foreign      (default: everything starts as foreign)
crate          → Transparent  (current crate is always transparent)
<--include>    → Transparent  (user whitelist)
<--opaque>     → Opaque       (user blacklist)
<--exclude>    → Invisible    (user exclusion)

In the default setup, everything outside the current crate is treated as Foreign and items in the current crate are Transparent. Note: there is no --foreign CLI flag, so this cannot be expressed directly via CLI flags — --opaque would make external items Opaque (signature only), which differs from Foreign for types (Foreign types with all-public fields are fully translated).

Pattern syntax

Patterns use a name-matcher syntax (charon/src/name_matcher/). Examples:

crate::module::item — matches this item and all its subitems
crate::module::item::_ — matches only the subitems (not the item itself)
core::convert::{impl core::convert::Into<_> for _} — a specific trait impl
_ or * — glob, matches any single path segment
{impl core::convert::Into<_> for _} works without the core::convert prefix, in this case we do a global search for impls.

Patterns are prefix matches: crate::foo matches crate::foo, crate::foo::bar, crate::foo::bar::baz, etc.³

Currently matching on inherent impl blocks isn’t supported, writing crate::module::_::method is the standard workaround.

Precedence

When multiple patterns match the same item, the most precise pattern wins⁵:

Longer patterns beat shorter ones.
Among equal-length patterns, a non-glob final element beats a glob.

Example with --opaque crate::module --include crate::module::_:

Item	Matching patterns	Most precise	Result
`crate::module`	`_`, `crate`, `crate::module`	`crate::module` (length 2)	Opaque
`crate::module::foo`	`_`, `crate`, `crate::module`, `crate::module::_`	`crate::module::_` (length 3)	Transparent

Note: pattern matching currently has limitations — e.g. it parses u64 as a path instead of the built-in type, and it is not possible to filter a trait impl (only its methods)⁶.

charon/src/ast/meta.rs:191 ↩
charon/src/bin/charon-driver/translate/translate_meta.rs:776-785 ↩
charon/src/name_matcher/mod.rs:51-125 ↩ ↩2
charon/src/options.rs:534-570 ↩
charon/src/name_matcher/mod.rs:189-221 ↩
charon/src/options.rs:112 ↩

Translating To/Executing With MiniRust

MiniRust is the semi-official specification for the runtime semantics of Rust. It’s an interpreter for a “condensed version” of Rust, whose execution determines exactly what the program does and what is/isn’t UB.

Charon supports converting its output to MiniRust’s input language! Pass --format=minirust to charon and you will get a json file that can be deserialized and run by MiniRust. Pass --run-with-minirust to charon and it will directly execute the main function of the translated crate using MiniRust.

A Charon function body is already pretty close to MiniRust, by the simple fact that both are based on MIR. The main difference is likely polymorphism: MiniRust only supports monomorphic code, and Charon will use its monomorphized translation when translating to MiniRust.

MiniRust also serves as the semantic definition of Charon: if there is doubt about the semantics of a statement, the translation to MiniRust in src/minirust.rs is considered authoritative.

Versioning

To get the version of the current Charon release, you can run:

charon version
# 0.1.259 (e4c4510d817097accb931fad0c14f357ce94066d)

The version number follows semver; though for now we are still in the 0.1.x versions. We hope to soon start providing better stability guarantees!

In parentheses is the git commit hash of the Charon source code that was used to build the binary. This is useful for debugging, to know exactly which version of the source code is being run. The version number is always bumped when the AST changes; however we reserve the rights to modify the translation without bumping the version number, e.g. for minor bug fixes.

What Charon Does For You

The purpose of Charon is to centralize the efforts of extracting information from rustc internals and turning them into a uniform and usable shape. Here are some things that Charon does once so you don’t have to do it yourself:

TODO: explain each item

Trait resolution (explicitly track how each trait bound was proven to hold);
Reconstruct expressions from all the various constant representations;
Hide the distinction between early- and late-bound lifetime variables;
Make non-overriden default methods in impl blocks appear as normal methods;
Handle trait method implementations that have a more general signature than as declared in the trait (WIP: https://github.com/AeneasVerif/charon/issues/513);
Represent closures as normal structs that implement the Fn* traits;
Represent VTables as normal structs stored in statics;
Represent drop glue via the Destruct trait;
Many useful post-processing transformations to make the output more usable; see the dedicated file.

Charon transformations

Charon has options to make the generated code easier to use. Some are currently not optional but could be made so on request.

Control-flow reconstruction

The MIR we get from rustc is a control-flow graph (CFG), where control-flow happens with gotos that can jump arbitrarily around the code.

Charon by default transforms this CFG into structured control-flow, i.e. with nested match/if/loop constructs.

To turn this off, pass --ullbc to charon (ULLBC stands for Unstructured LLBC).

`--hide-marker-traits`

This option removes mentions of the following built-in traits from the output crate:

core::marker::Sized
core::marker::Tuple
core::marker::Send
core::marker::Sync
core::marker::Unpin

This is a convenience option, meant to reduce noise for Charon consumers that output user-readable things.

Note that for historical reasons Charon removes mentions of the Allocator trait regardless of this setting. This should eventually be changed, open an issue if you have a need for it.

Note that today this is implemented by calling IndexMap::remove to remove the entry in the trait_clauses/trait_refs vectors. This abuses the confusion between newtype-indexed vectors and newtype-indexed maps we have in Charon, which can cause annoying footguns. See https://github.com/AeneasVerif/charon/issues/490.

`--remove-associated-types`

This option takes a pattern, and transforms the associated types of all the traits that match the pattern. This transforms code like:

#![allow(unused)]
fn main() {
trait Iterator {
  type Item;
  fn next(&mut self) -> Option<Self::Item>;
}
fn use_iterator<I: Iterator>(it: I) { ... }
}

into:

#![allow(unused)]
fn main() {
trait Iterator<Item> {
  fn next(&mut self) -> Option<Item>;
}
fn use_iterator<I: Iterator<Clause0Item>, Clause0Item>(it: I) { ... }
}

This transformation has limitations:

GATs cannot be transformed this way;
Some recursive traits cannot be transformed this way, e.g.:

#![allow(unused)]
fn main() {
trait Bar {
    type BarTy;
}
trait Foo {
    type FooTy: Foo + Bar;
}
// becomes:
trait Bar<BarTy> {}
trait Foo {
    type FooTy: Foo + Bar<Self::FooTy_BarTy>;
    // We need to supply an argument to `Bar` but we can't add a type parameter, so we add a
    // new associated type.
    type FooTy_BarTy;
}
}

We’re currently missing assoc type information to transform dyn Trait (https://github.com/AeneasVerif/charon/issues/123).
We currently don’t track bound lifetimes in quantified clauses properly (https://github.com/AeneasVerif/charon/issues/534).
Type aliases don’t have the correct clauses in scope (https://github.com/AeneasVerif/charon/issues/531).
We don’t take into account unicity of trait implementations. This means we won’t detect type equalities due to the same trait predicate appearing twice, or a trait predicate coinciding with an existing trait impl. See the dictionary_passing_style_woes.rs test file for an example.

Make implied bounds explicit

WIP: https://github.com/AeneasVerif/charon/issues/585

Current limitations of Charon

Charon is beta software. It works well but it is currently poorly documented, doesn’t support all the Rust features we’d like, and has several breaking changes planned in the near future.

Planned breaking changes

https://github.com/AeneasVerif/charon/issues/287
https://github.com/AeneasVerif/charon/issues?q=sort%3Aupdated-desc%20is%3Aissue%20state%3Aopen%20label%3AS-representation
Name matcher behavior likely to change in subtle ways (https://github.com/AeneasVerif/charon/issues/319).

Known unsoundnesses

https://github.com/AeneasVerif/charon/issues/583

Unsupported Rust features

Tracked here: https://github.com/AeneasVerif/charon/issues/142

Missing information in the translated output

Lifetime information about captured closure variables https://github.com/AeneasVerif/charon/issues/1040;
Precise lifetimes for higher-ranked trait predicates https://github.com/AeneasVerif/charon/issues/1143;
Lifetime information inside function bodies (not planned).

By-design limitations

Charon’s output contains little syntactic information. Stuff like scopes, or distinguishing between loop, while and for, is not kept; only semantic information is kept. This can impede lints. We do keep good spans for error reporting however.
It’s not possible to do trait solving on the output of Charon. Charon simply does not have all the type system logic needed to do that, nor would I want to try and reimplement that.

Internals

rustc_trait_elaboration

rustc_trait_elaboration is a subcrate of Charon, in charge of all the “trait proofs” logic (TODO: there should be a chapter explaining that). It’s meant to be a sort of extension to internal rustc APIs, hence the name.

The two main building blocks are:

TraitProof represents a trait proof object;
ItemRef is a reference to an item, identified by an Id and GenericArgs. The whole point of the crate is that we also compute a list of TraitProofs, which prove the item’s required predicates.

The crate is generic over the Id type used to identify items. It’s meant to be just like rustc’s DefId, but we do add fake extra Ids that don’t correspond to one, so the crate was made generic to support that.

Each provable predicate is identified by its ItemPredicateId. ItemPredicates contains the logic for computing which predicates each item has. This is the source of truth used everywhere else.

The important notion here is “required” vs “implied” predicates. Required predicates are those that must hold whenever we mention an item. E.g. fn foo<T: Clone> has a T: Clone required predicate. Most of them are like that. Implied predicates are those that we can derive from an item. These only occur in traits, and all where clauses of a trait as well as item bounds are implied.

The crate is a bit ad-hoc, it uses rustc APIs that aren’t meant to be used like that probably. Ideally we’d transition to using rustc’s recently-added “proof trees”, see https://github.com/AeneasVerif/charon/issues/1038.

Hax

Hax is a subcrate of Charon in charge of abstracting away most queries to rustc. Charon initially merged its rustc queries logic with hax-frontend from https://github.com/cryspen/hax, but eventually the usecases diverged sufficiently that we forked hax-frontend into a subcrate of Charon and reworked it. The name is kept for now but I’m thinking of renaming it to something like rustc_frontend.

The entrypoint of the crate is FullDef. A FullDef captures every single bit of useful information about a rustc item, which Charon then translates into its more uniform representation. It marks the boundary of rustc versus Charon: things that require rustc logic, like normalizing types, evaluating constants or solving traits should be done in hax and exposed through FullDef as much as possible.

The clever parts of hax are:

Trait proof solving, using rustc_trait_elaboration;
Constant evaluation and unevaluation, because rustc’s constant representations are a bit complex;
Monomorphization: FullDef can be created for a given item with or without a specific choice of generic arguments. If with arguments, then everything in the item is substituted and normalized, therefore monomorphizing the item. That’s how Charon can support monomorphization that’s guaranteed to give the same results as rustc;
Synthetic items: items in hax are identified by their hax::DefId. For the most part this is just a rustc DefId, but we also add a couple fictitious items, see synthetic_items.rs. These are used to simplify the generation of e.g. a concrete impl<A, B> Fn<(A,)> for fn(A) -> B item by Charon.

The rest is careful use of rustc internal APIs to avoid ICEs and find all the information scattered throughout the compiler.

charon_lib

charon_lib contains the full AST that Charon uses to represent a crate and its contents, along with (de)serialization logic, transformations, and all sorts of helpers.

Unlike the translation machinery that uses rustc internal APIs and therefore only works on nightly, this crate is a plain old Rust crate that compiles on stable (you just have to pass --no-default-features to cargo).

Charon translation

Running charon is split into two phases: translation calls into rustc APIs and constructs Charon’s representation for the crate and its contents, and transformations then transforms the pure-Charon AST into its final shape.

The main loop of translation is that we have a queue of items to translate, and we translate them one by one, enqueuing any new items we discover references to. Importantly translating each item is rather independent of another, and is done lazily; we must be careful when looking into self.translated_crate during translation, as it will likely be incomplete.

The main logic of translation is that each hax item gives rise to one or more Charon items. That’s for two reasons:

Monomorphization, where a given item is generated anew for each set of generic arguments it is used with;
Making implicit items concrete, for example a closure gives rise to a struct definition, up to three impl FnFoo for closure along with their methods and vtables, and finally a Destruct impl and method that carry the drop glue for the type.

TransItemSource identifies a unique Charon item. The RustcItem part distinguishes poly from mono items, and the TransItemSourceKind part distinguishes which Charon item we’re generating from a same hax item.

Beyond that, most of the translation logic is straightforward. The remaining complexity is in the handling of generics.

Translating generics

TODO: explain :3

The important entrypoints, that must stay in sync, are push_generics_for_def and translate_item_generics.

Charon transformations

See charon-driver/transform/mod.rs for a list of passes.

Frequently Asked Questions

I can’t find a definition/what’s this `<opaque>`

Try --extract-opaque-bodies; then try --start-from=path::to::definition.

Charon by default only translates the items of the current crate. Any items from other crates are treated as “opaque”, which means that they will be listed but without their contents (e.g. without a function body, or a type definition).

--extract-opaque-bodies is the hammer that removes this filter. Now all definitions reachable from the current crate will be translated in full.

That will still not include a foreign definition if it’s not used (even indirectly) by the current crate. To translate such a definition, you have to tell Charon explicitly, using --start-from=path::to::definition. Now instead of starting from the current crate, it will start from the definition listed. If you want both, pass --start-from=crate --start-from=path::to::definition.

Finally, note that --extract-opaque-bodies can cause a lot of code to be translated, which can be slow and/or hit some cases that Charon doesn’t support. You can have finer control over what gets translated using --include/--opaque.

See What Charon Translates for more details on how Charon decides what to translate and how to control it.

This trait doesn’t have all the methods it should have

Try --translate-all-methods.

By default Charon only translates a default method if it is used anywhere. E.g. this way Iterator only has next until another of its methods is used¹. --translate-all-methods instead always translates the full list of methods.

Charon is taking ages

Try --preset fast. This disables a bunch of checks, control-flow reconstruction, skips translating Sized and MetaSized, and uses postcard instead of json for the output. This significantly speeds up translation.

Overall Charon is structured around robustness over performance, so we won’t try to be competitive there. If however your crate takes 15 minutes to translate, do reach out to see if there’s anything we can do.

What is the difference between Charon and `rustc_public`?

Both projects aim at making it easy to analyze Rust code. Beyond that, they sit at two ends of the spectrum of “do extra work”: rustc_public intentionally stays close to the compiler’s representations, adding just enough abstraction to absorb changes as they occur between compiler versions.

In contrast, Charon aims for the most straightforward yet complete representation. For that, we do quite a lot of work of reconstructing information coming from various places in the compiler and hiding away any detail that’s not relevant to the semantics.

See What Charon does for you and Transformations to get an idea of the kinds of reconstructions we do.

How much can I trust what Charon outputs

Short answer: a fair amount

Longer answer: it depends on the kind of data. Some kinds of data are translated pretty much verbatim from what rustc gives us, and thus can be fully trusted. Conversely, some bits involve more Charon-specific abstractions, which leaves more room for errors.

Probably the most reliable part of Charon is the semantics of function bodies: not only is it converted rather directly from rustc’s MIR, but we run it against MiniRust’s test suite, and it is also interpreted and compared against Miri by the Soteria Rust project, which uses Charon.

Probably the least reliable part of Charon is lifetime generics: this is where we do the most work on top of rustc to get what we want; so mistakes there are likelier.

Another domain that doesn’t rely on rustc is layout guarantees. We compute them ourselves, based on the guarantees given by the Rust Reference.

Overall Charon is well-tested, and its authors are experts in the semantics of Rust. If you find a bug please report it, so we can incrementally make Charon more robust for everyone!

The whole “lazy method list” feature was pretty much made specifically for Iterator with its gajillion default methods and helper types. ↩

Keyboard shortcuts

The Charon Manual