Merging Hax and Charon

[R1kM]

This is a meta-issue tracking the roadmap to merge parts of Charon into the Hax frontend (written with @W95Psp and @sonmarcho). PRs related to this merge should reference this issue.

Current Workflow

The hax frontend extracts information from rustc's MIR and exposes an hax AST, which is not sufficient for Charon to build ULLBC, requiring additional rustc queries in Charon. The hax AST is intended as an unopinionated version of MIR; ULLBC is a clean-up, simplified version that preserves the general structure, but makes opinionated choices about some representations (e.g., a unique representation for ADTs). Finally, LLBC is a transformation from ULLBC that performs control-flow reconstruction, leading to a "structured" MIR.

Goal

We aim for a clear separation between the different phases (rustc MIR, hax AST, ULLBC, LLBC). To do this, we propose a refactor of hax and charon so that Charon does not require calls into rustc, instead purely consuming the hax AST. The advantages are the following:

• This will simplify maintenance of both projects wrt rustc: only hax will have to track changes to rustc (while Charon will track changes to hax)
• This will reduce the number of needed entrypoints into hax, simplifying testing hax code paths: currently, Charon requires calls into hax on subexpressions and sub-ASTs, thus requiring fine-grained hooks into hax; as a consequence, testing these hooks in isolation is currently tricky.

Proposed Roadmap

Achieving this goal requires the following steps:

• Add more information to the hax AST to provide all required constructs to Charon to remove the need for "localized" rustc queries on items (e.g., the discriminant of an enum variant).
• Remaining rustc queries in Charon will relate to traversing crates. We will refactor Charon to move these to a first stage of Charon, which will be followed by the hax AST to ULLBC translation.
• Once separated from the translation, these queries will then be moved to hax, removing rustc queries from Charon. hax currently relies on similar queries for crate traversal, but with different options (e.g., ignoring external declarations). Supporting hax- and charon-compatible versions of queries will require the parametrization by "options", which will facilitate the development of future extensions and use cases that might arise.
• ULLBC and LLBC (and their translations from the hax AST) will remain in Charon at the end of this work.

Before this, we intend to upgrade hax and Charon to the latest rustc (https://github.com/hacspec/hax/issues/224, https://github.com/AeneasVerif/charon/issues/182)

[clarus]

There is also the https://github.com/formal-land/coq-of-rust project in this space that could be useful to merge, too, as suggested by @spitters . It uses THIR as input, so this seems to be a major difference from Hax and Charon, which use MIR, as I understand. Also, we do not follow information from the borrow checker and put everything in a generic monad. While doing the proofs, we basically make and prove the transformation that Aeneas is doing by hand in Coq. So, eventually, coq-of-rust should be completely replaced by Aeneas, at least for the safe parts of Rust.

Maybe coq-of-rust is too different to share anything for now.

[W95Psp]

Hi @clarus! Actually Hax also uses THIR, so it might indeed be interesting to chat :)

The "frontend" of Hax is the part that links into Rustc. It mirrors Rust internal ASTs to hax variants of those ASTs in which all the information you might want is there already.

For instance, on a method call, you get an expression that constructs the precise impl you call onto. Another example: instead of opaque IDs for sub-expression, the mirrored THIR/MIR contains directly sub-expressions. The aim is that when you get the hax AST, you can just work with it with no further interaction with rustc.

The frontend of hax supports both THIR and MIR (this issue is partially about improving the MIR output so that Charon can rely on it and stop interacting with Rustc)

[clarus]

Hi! OK, this is very interesting to have the ability to get the precise impl that you are calling! That would be useful for us to have that. This would require an effort on our side to rewrite our code and, I guess, also to contribute to this project for the specific parts we need that might be missing.

In the short term (the coming month or two), we do not have the bandwidth, but after we should get a look!