Expose charon as a rust library

[Nadrieril]

We'd like other rust users to be able to use Charon code. This may involve:

• Make a library that exposes the ast types and helpers;
• Detangle most micro-passes from rustc and make them available in the library;
• Make the dependency on rustc optional behind a feature flag.

[Nadrieril]

#284 does most of that. charon-lib (which includes the ast definition and the control-flow reconstruction) should be pretty compatible with other rustc nightlies now. The only thing that remains would be to replace our usage of rustc internal crates for error reporting.

[zhassan-aws]

Did you have plans/thoughts on how Charon can be restructured so that the library can be included without including the toolchain-dependent crates in the dependencies (e.g. hax-frontend-exporter)?

Currently, including the Charon library as a dependency brings in the dependencies used in the binaries as well.

Unfortunately, cargo doesn't allow specifying binary-specific dependencies easily:

rust-lang/cargo#1982

The workarounds from what I understand are:

1. Use a workspace, and use different packages for the library and the binaries
2. Make hax-frontend-exporter an optional dependency under a feature that is only used for the binaries. One would need to pass --features X when building the binaries though.

[Nadrieril]

Oh yeah, I was thinking we'd add a feature flag. Either is fine probably.

[Nadrieril]

Alright, this should now work on many nightly compilers:

[dependencies]
charon = { git = "https://github.com/AeneasVerif/charon", default-features = false }

[Nadrieril]

The most interesting modules are ast which contains all the ast definitions, and transform which contains the code for the various transformations we do after translation, including control-flow reconstruction.

I believe the current state is good enough to close this issue, lmk if not.

[zhassan-aws]

Awesome, thanks @Nadrieril!

[zhassan-aws]

Looks like a hax dependency got added to the library recently:

charon/charon/src/ast/types.rs

Line 5 in 39c9404

use hax_frontend_exporter as hax;

This was introduced in 316a376

Is there a way around it? I'm happy to contribute if you can provide some guidance.

FYI, I opened a PR in Kani that is the first step in adding an LLBC/Aeneas backend: model-checking/kani#3514. Thanks for making this possible!

[Nadrieril]

Oops, my mistake. I don't know an easy way to ask rust to enforce binary-only dependencies. Give me just a minute to fix that.

[Nadrieril]

Fixed in #360

[zhassan-aws]

Thanks for the quick fix!